IW Meeting 2009-04-16

From Inference Web

Jump to: navigation, search




  • combine proof algorithm
  • proof combine metrics
  • interop discussion
  • general funding


null problem (reported by paulo)

Thu, Apr 9, 2009 at 3:00 PM

I am using ProbeIt to view the example proof http://inference-web.org/proofs/tptp/Solutions/SEU/SEU368+1/EP---1.0/combined20.owl#answer used during the meeting and I could not find "null". Could you please point it out to me? I need to fix any "null" problem.

There is one nodeset A with uri of http://inference-web.org/proofs/tptp/Solutions/SEU/SEU368+1/EP---1.0/combined20.owl#ns_265_antecedent_75 has no conclusion string. It came from the embedded "inference" from the tptp cnf of:

<NodeSet rdf:about="http://inference-web.org/proofs/tptp/Solutions/SEU/SEU368+1/EP---1.0/combined20.owl#ns_265_antecedent_75">
    <pmlp:hasRawString rdf:datatype="http://www.w3.org/2001/XMLSchema#string"
    > </pmlp:hasRawString>                                    </pmlp:Information>


cnf(265,negated_conjecture, ( the_carrier(rel_str_of(esk14_0,inclusion_relation(esk14_0))) != esk14_0 | the_InternalRel(rel_str_of(esk14_0,inclusion_relation(esk14_0))) != inclusion_relation(esk14_0) ), inference(rw,[status(thm)],[inference(rw,[status(thm)],[253,250,theory(equality)]),250,theory(equality)]), [unfolding]).

From this cnf, we create 2 nodeset, the nodeset A and nodeset B with uri of http://inference-web.org/proofs/tptp/Solutions/SEU/SEU368+1/EP---1.0/combined20.owl#ns_265. The nodeset A is the antecedent of nodeset B. We did not put any conclusion string for nodeset A is to respect the original tptp cnf which has no formula for the embedded inference.

Please let me know if you think this should be handled differently.


  • when there are two inference rules associated with one step. Cynthia's translation create two inference steps, each associated with an application of a rule. Some time we know the order of applications of rule.
  • when two rules have been applied in sequence, and we don't know the intermediate result. we currently generate two steps, one of which has an empty conclusion.
  • we may in the future add an abstraction step to show the composition of rules.

PML property (cynthia)

Here are the properties in question:


  • a. Have we decided on replace 1 with 2?
  • b. I have just become aware of 3. It is going to stay isn't it?
  • c. I suggested to remove the maxCardinality=1 for fromAnswer. The reason is that if a inference step can be used in combined proofs, it can conclude not only the original answer but also the answers of combined proofs, therefor fromAnswer can point to multiple proof answer root nodesets.
  • d. Now we have both hasOriginalProof and fromAnswer properties, how do we use these two together.
  <owl:ObjectProperty rdf:about="&pmlj;isExplanationOf">

	<rdfs:label xml:lang="en">explains</rdfs:label>
    <rdfs:comment xml:lang="en">links to a node set (and its antecedents) that is explained by the present node set. 
     This is used for connecting the orginal justifications to the NodeSet that abstracts this node set (and its antecedents).
    <rdfs:domain rdf:resource="&pmlj;NodeSet"/>
    <rdfs:range rdf:resource="&pmlj;NodeSet"/>


  • keep hasConfidenceValue
  • probably add hasOriginalJustification (replacing hasOriginalProof), and replace isExplanationOf
  • we don't have decision so far, and we will come back in two weeks.
  • paulo is not willing change PML


  • paulo will read Combine proof example 2 and response. This will be done by April 23
  • deb will miss the meeting the next week.
  • cynthia add hasConfidenceValue to PML API, to synchronize with PML ontology
  • we will come back to #PML property in two weeks.
  • Li and Cynthia work stable version of IW Search (separately for pmlp, and pmlj)
  • Deb and Li talk to Peter on SPCDIS search requirements
  • PMLP in semantic wiki
  • Paulo read open provenance model paper. http://eprints.ecs.soton.ac.uk/16148/1/opm-v1.01.pdf
  • Deb will schedule with Honglei on his trip to RPI
Facts about IW Meeting 2009-04-16RDF feed
Date16 April 2009  +
Personal tools