IW Meeting 2009-02-19

From Inference Web

Jump to: navigation, search



  • 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


  • 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)

Mizar proof (geoff)


  • 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."
Facts about IW Meeting 2009-02-19RDF feed
Date19 February 2009  +
Personal tools