IW Meeting 2009-02-19
From Inference Web
2009-02-19
agenda
- website moved, will replace inference-web.org main site in a month
- backtracking on combined proof (overview)
- combine proof strategy
- Mizar proof translation
- backtracking on merged proof
notes
- Deb missed this telecon
- Geoff will be in bay area between 23-26 (that meets AAAI spring symposium), may be a short meeting there.
backtracking on combined proof (paulo)
- combine proof has similar flavor to abstracted proof
- the combined proof should point back to the original proofs
- example limitations
- for a proof combining multiple proofs fragments from difference sources, trust is a problem
- the combined proof should not damage existing proofs.
- it is hard to navigate from the combine proof to the original proofs
- User:Geoff This problem (which is valid) seems to suggest a change to the PML, rather than the concept of combination, right? Need PML upgrade to record proof source history. From the point of view of analysing any proof (combined, whatever) we are not affected, right?
combining proof (geoff)
- http://inference-web.org/tmp/012009.html
- bugs: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FCSR%2FCSR014%2B1%2FMetis---2.1%2Fcombined20.owl%23answer - something is wrong with the counting number
- new problem: compute graph difference, http://mathworld.wolfram.com/GraphDifference.html. motivations: (i) detect topological difference of two proofs; (ii) detect the difference between the combined proof and the original proof (this can be partially done by backtracking, concerns may arise on the space need to store the backtracking information- we may not able to track all links back to all original proofs)
Mizar proof (geoff)
- example mizar proof for translate: http://www.tptp.org/MizarTPTP/TPTPProofs/xboole_1/xboole_1__t1_xboole_1
todo
- discuss backtracking proof next week (paulo)
- compute graph difference (honglei)
- geoff will provide examples, "I give two proofs, wth baled nodes, compare them, and chr=aracterize the differences into one of the cases in the IJCAI paper."
