# IW Meeting 2009-02-26

### From Inference Web

2009-02-26

## agenda

**review** IW Meeting 2009-02-19

**backtrack provenance of combined proof**

**mizar translation**
I have generated PML proofs for Mizar xboole_1 and newton as Geoff suggested, almost.
All xboole_1 proofs were generated smoothly, but a bounch of newton proofs failed.
The failed newton proofs are t5, t11,t30-t32, t35, t36, t38-t41, t43, t45,t47,t50,t51,t78,t79,
t81,t86,t96-t99 and t101. From what I can see, they all have larger size than most of the
others. I am wondering if they are also different structurally. Here is the url leads to the
Mizar proofs: http://inference-web.org/proofs/tptp/MizarProofs/

Another thing is that I also used the program Geoff sent to generate pml query(problem) strings. The query strings I have checked are long. For example, take a look of: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FMizarProofs%2Fxboole_1%2Fxboole_1__t1_xboole_1.owl%23answer

In a previous meeting I said I would generate a report for each combined proof. I've just got the first cut of it. Please take a look of an example: http://inference-web.org/proofs/tptp/Solutions/SWC/SWC028+1/Metis---2.1/combined30.tptp.report.html

**honglei graph diff**

**combine proof report**

**PML on Wiki**
http://tw2.tw.rpi.edu/wiki/r2d2/index.php/Mizar_Test1

**dump term equivalence relation**

## notes

**backtrack provenance of combined proof**

- is_explanation_of in pmlj
- rename to has original proof
- remove max cardinality
- make it a fully ordered list

**equivalence relation**

- http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.0/equalNS.owl
- equivalence semantics is directional

## todos

- todo - cynthia will generate an example and go over with paulo BEFORE the next meeting.