IW Meeting 2009-07-30

From Inference Web

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

Contents 1 agenda 2 notes 2.1 improved proof 2.2 mizar proofs 2.3 tptp to pml translation 2.4 web portal of translated tptp 2.5 probe-it 3 action item

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?
  • SWPM:
    • (i)james (inference web workflow showcase);
    • (ii) jie/li semantic history;
    • (iii) li provenance requirement

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