IW Meeting 2009-02-05

From Inference Web

Jump to: navigation, search



  • updates
  • clarify proof quality metric
  • clarify datasets



  • combined proof in ProbeIt
  • IDV fixed, not yet back to proof
  • geoff need automated analysis provided in IDV
    • need to compare two proof in whole, instead of looking into the steps
  • geoff asked the linked to the demo page: http://inference-web.org/tmp/012009.html

identify combinable proofs

  • all TPTP data has been translated into PML
  • we are still working on choosing proofs to combine. we use heuristics to identify combinable proofs.
  • do we need automated methods to detect combinable proofs?

compute equivalence of formula

  • We probably should not spend much time on computing equivalent formulas (identifying merge-able nodes), unless we can find good heuristic in the domain of logical forms. Co-reference identification in information retrieval and ontology mapping in Semantic Web are long-standing hard problems.[honglei]

evaluate and compare proof quality

  • use IR methods to Proof evaluation
  • Graph structural analysis is typically NP-complete, for example, graph homomorphism. We may treat subset measure and different source measure separately, since they are disjoint events.

we need the following functions

  • f(proof) \in number: bring a total order to all candidate proofs
  • g(p1,p2) \in number: bring a total order to any pair of candidate proofs


  • todo:geoff will identify groups of combinable proofs (proofs in each group are ready for formula equivalence computation function supplied by Geoff)
Personal tools