# IW Meeting 2009-07-30

### From Inference Web

- 2009-07-30
- IW Meeting 2009-06-25

## Contents |

## agenda

- round on status
- cynthia:
- more examples of converted TPTP proof

- li/honglei: linked proof:
- publication plan: CADE (Feb 2010), WWW(Nov 2009), IEEE intelligence (success story)
- (i) TPTP on Semantic Web (done)
- (ii) directed hypergraph formalism; (done)
- (iii) combine algorithm; (working)
- (iv) complexity of search space. (done)
- (v) evaluation, metrics of proof; (working)
- (vi) more computations (todo)

- paulo:
- portal
- person registration
- resource registration (including grouping by project)
- basic collaboration infrastructure
- identified requirements
- iw-search integration (??)
- others?

- derivation data visualization (probe-it)
- local view improvement
- viewer registration documentation
- requirements
- new viewers for fof and cnf?
- fof (and cnf) to english translation?

- portal
- SWPM:
- (i)james (inference web workflow showcase);
- (ii) jie/li semantic history;
- (iii) li provenance requirement

- cynthia:

## notes

### improved proof

> http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ016-1/Metis---2.2/combined.tptp Very nice, and quite interesting. All of the real "reasoning" steps from the Metis proof have been replaced - only boring syntactic steps of Metis have been left behind. The powerful hyperresolution steps of SOS, and combined resolution-demodulation steps of Vampire are so much chunkier than the binary resolution steps of Metis that they replace al parts of the Metis proof. It's noteworthy that the original Vampire proof is better than the original SOS proof, which is beter than the combined proof (which is based on the Metis proof), which is beter than the original Metis proof. Can you try combining just the Vampire and SOS proofs - I suspect there will be no improvement - the Vampire proof cannot be improved by the SOS proof. > http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ016-1/EP---1.0/combined.tptp Again, interesting. Here we see the same effect as above ... SNARK's combined hyperresolution+rewriting steps trump EP's separate binary resolution and rewriting steps. In both these cases, it is reasonable to claim that the proofs using the larger inference steps are more natural for a human. Aha! ... when I use my proof synopsis tool to identify the "interesting" steps in the original EP proof, and then create a synopsis by bypassing the more boring steps, I get almost exactly the combined proof! That's very nice - the two completely different approaches lead to the same optimized proof. The orginal Vampire proof is still better by node count, but looking carefully, its last step is a very large one - it seems too large to be natural for humans. That leads us to an observation about quality metrics ... A proof that has too few inference steps (because it takes very large inference steps) is worse for humans than one that takes the "right size" steps. Similarly, a proof that has too many inference steps (because it takes very small inference steps) is also worse that one that takes the "right size" steps. This observation is what Chris Benzmuller observed in his response to my email asking ATP people for opinions about proof qualities - quality is in the eye of the beholder. So, here's an idea ... maybe we should analyse proofs to find conclusions that are in the majority of proofs, and find proof combiations that include all/exactly those conclusions?

### mizar proofs

cynthia - asks if we want more mizar problems. Geoff has given cynthia the pointer on geoff's web site. cynthia has only done those starting with a-c but stopped there.

### tptp to pml translation

- massive data conversion: new computer? use grid/super-computing
- find bottle neck: JENA, TPTP parser, 20,000+ parallel job
- what is the interface language of super-computer

### web portal of translated tptp

- data portal: list of pml for tptp, some kind of index

### probe-it

- new interface added probe-it, show the detailed conclusion in popup/hoover tooltip
- local view added
- porting IDV features...

## action item

- cynthia and geoff, proof self improvement
- cynthia - asks if we want more mizar problems. Geoff has given cynthia the pointer on geoff's web site. cynthia has only done those starting with a-c but stopped there.
- todo - geoff send deb workshop proposal today; deborah respond no later than fri am - probably this afternoon
- paulo - visualization of combined proof, probe-it
- paulo - portal