IW Meeting 2009-08-27

From Inference Web

Jump to: navigation, search

notes

TPTP proof combine demos

problem set notes pml generation mapping file generation combine
TPTP
  • CRS selected by Geoff
  • SWC selected by Geoff
  • ANA all (except some big ones)
  • GEO all (except some big ones)
  • PUZ all (except some big ones)
  • combine solutions selected from one problem
  • selected by Geoff
up to date in place done
Mizar Proofs
  • combine solutions selected from one problem
  • like human generated
  • proof structure more complicated
  • combine space is large
converted, out of date todo experiment on small set
SEU
  • combine many solutions selected by Geoff
  • combine space is large
converted, out of date todo experiment on small set


demo template

  • title
  • screen shot
  • description
  • list of pml files (corresponding TPTP solution files) to be combined
  • the mapping file
  • the combine result (new PML file and new TPTP)
  • live iw browser demo link

demo plan

  • demo1: after conversion, we found some issues in the proofs generated by Metis (they didn't record some steps), and we feedback our observations to the developers and causes a new new version of Metis.
  • demo2: self-improvement for one solution
  • demo3: helper-improvement

evaluation plan

  • count unique CNF formula show up in a solution, so we can tell if the combineable nodes are actually combined after self-improvement


issues

  • correctness of combined proof
  • we should not combine proofs generated by two different versions for the same reasoner
  • restrictions
    • collapse of false path
    • use of axiom, replace a intermediate node with an axiom

action items

  • paulo will run a demo on probe-it the next week
  • question geoff. restriction on combine: leaf node (axiom) can only be combine with the node derived from it
  • generate mapping files for pml solutions as soon as possible. (we may ask a student at RPI work it out. Cynthia will think about it.)
  • cynthia, suggest concrete demos instances for demo1 to demo3
  • cytnhia, write down criteria of correct proof
Personal tools
Navigation