# IW Meeting 2009-04-02

### From Inference Web

2009-04-02

## agenda

- previous meeting: IW Meeting 2009-03-24
- mizar proof, clean up translation problems in newton (cynthia, geoff)
- generate one conclusion mapping file (pairs of conclusions which are the same) for each problem (cynthia)
- realize the metrics in combine algorithm (li)
- soundness of this approach (honglei)

- other issues
- combine metrics IW_Meeting_2009-03-24#metrics
- ijcai paper - evaluation

## notes

mizar proof

- memory problem is related to jena
- cynthia has 6000 mizar proofs ready, http://inference-web.org/proofs/tptp/MizarProofs/
- the current proof translation take a lot of time, still running

benefit of TPTP-PML translation

- During TPTP-PML translation, we've found some dangling fragments in proofs (we see a forest but not a DAG)
- cynthia has combine the forest into a DAG

cynthia's mapping files

http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.0/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Faust---1.0/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Metis---2.1/ http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Otter---3.3/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SNARK---20080805r005/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SOS---2.0/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SPASS---3.01/equalNS.owl http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Vampire---9.0/equalNS.owl

li's combine proof

- code tested in synthesized dataset
- testing on the "PUZ001-1" , http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/

honglei's complexity analysis: "sharp P"

## action

- (geoff) will work on the jaccard metrics
- (honglei and Li) will work on the complexity analysis
- (Li) work out the first ATP combine problem
- for the next week Deb and Li will be in-transit
- (cynthia) work on mizar translation, and update ATP proofs