# IW Meeting 2009-02-05

### From Inference Web

## Contents |

## agenda

- updates
- clarify proof quality metric
- clarify datasets

## notes

### updates

- 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

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