IW Meeting 2009-08-27
From Inference Web
- 2009-08-27
- IW Meeting 2009-08-20
notes
TPTP proof combine demos
| problem set | notes | pml generation | mapping file generation | combine |
|---|---|---|---|---|
| TPTP |
| up to date | in place | done |
| Mizar Proofs |
| converted, out of date | todo | experiment on small set |
| SEU |
| 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
