# IW Meeting 2009-03-12

### From Inference Web

2009-03-12

## Contents |

## Agenda

1. review last meeting IW Meeting 2009-03-05

2. review TPTP-IW research problems

3. identify combinable proof (cynthia) - mizar proof

- http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FCSR%2FCSR020%2B1%2FSPASS---3.01%2Fanswer.owl%23answer
- http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FSWC%2FSWC028%2B1%2FMetis---2.1%2Fanswer.owl%23answer
- http://browser.inference-web.org/iwbrowser/BrowseNodeSet?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FCSR%2FCSR014%2B1%2FSPASS---3.01%2Fanswer.owl%23answer

4. metrics for proof quality (Geoff) -

Objective 1: Make theorems easier to trust.

+ Note I do not say "make them more trustworthy" - all sound proofs are 100% trustworthy. I am placing the emphasis on the user's perception.

+ A theorem that is proved using a subset of the axioms used by an earlier proof becomes easier to trust, because you have less axioms to trust. And axioms are something you trust - they have no "logical" justification. Thus, if we can find a combined proof that uses a subset of the axioms used by an existing proof, the theorem has become easier to trust.

+ A theorem is easier to trust if has been proved from two different sets of axioms. The greater the difference, the easier it gets, i.e., a greater Jaccrd distance between the set axioms sets is better. Thus, if we can find a combined proof that has a high Jaccard distance from existing proofs, the theorem has become easier to trust.

+ The above two can be combined, e.g., given proofs A and B proved from axioms Ax(A) and Ax(B), if we can find a combined proof C such that Ax(C) is a subset of Ax(A), and Ax(C) has a high Jaccard distance from Ax(B), we have done good.

Objective 2: Make proofs more interesting and easier to understand

+ This is kinda what we are doing already, by finding combined proofs that are smaller than existing proofs. Smaller proofs are generally easier to understand. That's called "Obviousness" in my interestingness criteria.

+ We can use other measures adpated from my interestingness criteria. We have to avoid criteria that are context dependent, because the context changes during the combining process. Two that will work are: - Weight - the number of symbols in the subproof - Complexity - the number of distinct symbols in the subproof

5. backtrack provenance

6. stanford meeting schedule

7. stable IW Website

- convert IW website to wiki based
- IW registry
- tomcat crash and memory overload of IW web services
- new IW server

8. Evolve PML Ontology on Wiki

- I just imported PML2 ontology into another wiki. This could be a good step for us to evolve pml ontology
- PMLP http://tw2.tw.rpi.edu/wiki/r2d2/index.php?title=Special:SearchByProperty&offset=0&limit=100&property=Member+of&value=Http%3A%2F%2Finference-web.org%2F2.0%2Fpml-provenance.owl
- PMLJ http://tw2.tw.rpi.edu/wiki/r2d2/index.php?title=Special:SearchByProperty&offset=0&limit=100&property=Member+of&value=Http%3A%2F%2Finference-web.org%2F2.0%2Fpml-justification.owl

notes:

- this site is not final, once you agree the layout, I will move all those pages to inference-web.org
- the dump is done by java code, should be easy to managed by cynthia
- I also dumped OWL,RDF,RDFS, PML-DS, you should be able to surf to their pages.

## Notes

### Paulo's example of backtracking

P1: D1([di1->C1]) ;C1([ci1->B1]);B1([bi1->A1]);A1([ai1(s1)]) P2: D2([di2->C2]) ;C2([ci2->B2]);B2([bi2->A2]);A2([ai2(s2)]) conclusions of C1 and C2 are the same

After the merge we have a forrest F1:

Forrest F1: D3([di1->C3]);D4([di2->C3]);C3([ci1->B3][ci2->B4]);B3([bi1->A3]);A3([ai1(s1)]);B4([bi2->A4]);A4([ai2(s2)]) isFromAnswer: ci1 in C3 points to D3 and ci2 in C3 points to D4 hasOriginalProof mappings: D3->D1;D4->D2;C3->[C1,C2];B3->B1;A3->A1;B4->B2;A4->A2

Possible proofs derived from F1:

DP1: D3;C3;B3;A3 DP2: D3;C3;B4;A4 DP3: D4;C3;B3;A3 DP4: D4;C3;B4;A4

Now you ask the following: Which derived proof is the best? DP1, DP2, DP3 or DP4?

Now, what happend if we want to merge two forrests or a forrest and a proof?

F1: D3([di1->C3]);D4([di2->C3]);C3([ci1->B3][ci2->B4]);B3([bi1->A3]);A3([ai1(s1)]);B4([bi2->A4]);A4([ai2(s2)]) P3: D5([di5->C5]) ;C5([ci5->B5]);B5([bi5->A5]);A5([ai5(s5)]) conclusions of B4 and B5 are the same

### Geoff's combine proof algorithm

keep_going = TRUE while (keep_going) { keep_going = FALSE foreach proof[A] { best[A] = proof[A] } foreach proof[A] { foreach proof[B] { proof[A-B] = greedy_combine(proof[A],proof[B]) if (proof[A-B] is better than proof[A]) { best[A] = proof[A-B] keep_going = TRUE } if (proof[A-B] is better than proof[B]) { best[B] = proof[A-B] keep_going = TRUE } } } foreach proof[A] { best[A] = proof[A] } }

### Geoff's metrics

who will appreciate those issues

- 1.a people who are skeptical on the combined proof, given they trust proofs from different sources differently, sources are mutually reinforcing each other
- 1.b same as 1.a, given they trust axioms equally (assume all axioms from one source)

## Todo

- todo - geoff write how to get the effect of all at once combination by doing a pairwise combination
- todo dlm - think about nsf interop proposal for our work
- todo Li and Geoff work on the combine algorithm
- todo - geoff will make up a small example that illustrates example 1. (cats dogs rats apples)
- todo - cynthia and li talk about memory management on onto
- todo cynthia and li talk about what what should go in the final configuration on the stable machine for iw.
- todo - cynthia and li talk about iw search
- todo - cynthia and li send an email with notes on the meeting