# IW Meeting 2010-02-25

### From Inference Web

- 2010-02-25
- IW Meeting 2010-02-18

## Contents |

## agenda

### TPTP-IW Project

- todo - geoff look at equivalence of formula with skolem symbol renaming
- we wrongly assume two clauses are equivalent, the code cannot be fixed immediately,
- however the bug lead to an underestamation of difference

- todo - Li work on upcoming work. Linked_Proofs_Dataset#Upcoming_feature link to the portion of cynthia's work that is stable. discussion on how to break up the results.
- done
- change file extension ".txt" => ".csv" ?
- we've doen with Axiom, and geoff is now looking into the CNF

- todo - cynthia provide a page that has stable info and at the moment we believe that is the axiom line.
- todo (done) - geoff provide definitions of leaf nodes, see Linked_Proofs_Dataset#Glossary
- geoff has provided conceptual definition, but we still need operational semantics.
- can we have a SPARQL query that identifies the axiom ?

1. Currently, we only produce analysis on fof problem proofs. 2. Each analysis uses proofs of same problem. 3. A proof axiom is defined as a tptp formula with no parent which is the same as a PML NodeSet with no antecedent. 4. For a proof to be qualified to participate in the analysis, it cannot have any cnf proof axiom except if the axiom has source of "introduced". 5. A fof proof axiom is counted in the analysis only if it can be found in problem’s axiom set. One exception is that if a fof proof axiom has role of “negated-conjecture” and its correspondent “conjecture” can be found in the problem, this fof is also counted. 6. The conjecture formulae in problems are treated separately from their “logically equivalent” axioms.

* http://inference-web.org/tmp/formulau/SEU140+1/axiomUsed.html * the conjecture is store in pml:Query, http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FProblems%2FSEU%2FSEU140%2B1%2Fquery.owl%23query * we should probably list all axioms in pml:Query

* a disqualified proof will have a CNF leaf node which does not have "introduced" in its raw string * any leaf nodes in a qualified proof are one of the following (i) FOF (any kind, such as conjecture,negated conjecture, axiom), (ii) introduced CNF * a proof's axioms are essentially the leaf nodes * we only care the following formulae in axiom analysis: (i) it is the proof's axiom: (ii) it is FOF formula; (iii) it is an element of the problem's axioms, the conjecture of the problem, or the negated conjecture of the problem

- todo - cynthia write up how the analysis was done, Linked_Proofs_Dataset#Glossary
- todo - add statistics like http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=PUZ. (number of historical proofs , number of current proofs)
- we expect to see it at http://browser.inference-web.org/tptppml/ListProof?scope=problem&category=Problems&domain=SEU
- question: what about those problems with no proofs indicated by the status field in problem file?

- todo (done) - replace SET001-1 to PUZ001+1, or SEU140+2
- where to get

### iw:EMSQMS 2010 proof quality

### Inference Web Website updates

- todo - cynthia make sure http://inference-web.org/wiki/Tools has links that resolve correctly (ask li or patrick if needed)
- the TW SVN is ready for use, cynthia should contact Stephan to start using SVN ("private" part for our internal code control and "public" part of our API API jar release)
- todo (done) - cynthia will redirect http://iw.stanford.edu/iwregistrar/ to http://registrar.inference-web.org/iwregistrar/
- todo - cynthia let paulo and nick know what is needed for her to help. she does have a lot to do so as much as nick can do is appreciated
- todo - paulo add his project to project page, and review tools and demo page.
- todo - james generate video demo for wine agent
- todo - add the spcdis search to inference-web.org.
- todo (done)- fix links for iwsearch and pml validator

### PML Ontology Project

- todo - paulo propose change to PML ontology PML_Ontology_Update_Request_2

- after todo review when deborah joins, discuss PML presentation on provenance incubator group

## notes

paulo introduced his colleague professor

TPTP-IW project

- change output presentation for http://inference-web.org/tmp/formulau/SEU140+1/cnfUsed.html, move the first column to the last column

March 12, 2010 PML presentation in provenance incubator, we need significant updates on the website

1. Inference Website update 1.1 Inference projects 1.1.1 Paulo's projects 1.1.2 related funded projects 1.2 PML documentation 1.2.1 PML primer update http://inference-web.org/2007/primer/ 1.2.2 PML API documentation 1.2.3 PML Ontology documentation 1.2.4 How to generate PML 1.2.5 PML Examples with Scenario Description 2. PML ontology update 2.1 better support SPARQL, decouple recursive list 2.2 renamed concepts 3. PML tools 3.1 PML validator 3.1.1 (jiao) renovate PML validator 3.1.2 validate PML in triple store 3.2 PML API 3.2.1 broken PML API (use foaf:Person, multiple conclusions) 3.3 TPTP combine 3.4 IWbrowser etc. 4. upcoming events 4.1. PML presentation in Provenance incubator, March 12, 2010

## action items

- PML primer (Paulo will meet with both Nick and Jitin by tomorrow March 2, 2010; Deb will talk to Tim)
- PML examples and scenarios, need diversity (e.g. Source Usage), Tools#Datasets