Understanding the justification

This page is a continuation of Installation and Tutorial and describes how the PML dumped from Step 5 serves as a justification for the conclusion isCool(nick).

Finding the Root

The value of URI points to the root NodeSet of our justification tree.

5 ?- why(isCool(nick),URI).
Generating proof tree file at ./pml/pml-proof.owlconjunction found
URI = "https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_1".

If we open the file ./pml/pml-proof.owl and navigate to the URI https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_1, we will find the RDF/XML segment of the root NodeSet (e.g., the final proof step of our justification tree):

<NodeSet rdf:about="https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_1">
  <hasConclusion>
    <pmlp:Information>
      <pmlp:hasRawString rdf:datatype="http://www.w3.org/2001/XMLSchema#string">isCool(nick).</pmlp:hasRawString>
      <pmlp:hasLanguage rdf:resource="http://inference-web.org/registry/LG/English.owl#English"/>
    </pmlp:Information>
  </hasConclusion>

• We see that the conclusion isCool(nick) is associated with our root NodeSet, which makes sense since it was the conclusion we are trying to justify. If we want to understand how this conclusion is derived, we must look to the pmlj:InferenceSteps associated with this NodeSet.

Multiple Justifications for Single Conclusion

Consider the disjunctive rule in the program [isCool.pl]:

isCool(X) :- isPopular(X); isComputerScientist(X).

• In order to prove that object X is cool, Prolog only needs to prove whether object X is popular or whether object X is a computer scientist, but not both. If Prolog can prove that object X is popular, then it does not have to (and won't) prove if X is also a computer scientist.

• However, it might be useful for a user to know if X is also a computer scientist, and so our program [prolog2pml.pl] will evaluate isComputerScientist(X) even in light of knowing that X is popular.

• In our PML example, we have a single conclusion, isCool(nick), that is justified by the two statements, isPopular(nick) and isComputerScientist(nick), since both are true. In PML, we can encode this scenario where a single conclusion can be justified by different statements by saying that a NodeSet's Conclusion can be derived from multiple InferenceSteps. Our program prolog2pml.pl uses this feature of the language to provide a full justification in the case of disjunctive rules.

Justification 1* Using Prolog's Hyper Resolution, we have the proof:

[isCool(X) :- isPopular(X); isComputerScientist(X)] and [isPopular(nick)]
-------------------------------------------------------------------------
                     [isCool(nick)]

This part of the proof is encoded by the RDF/XML below:

  <isConsequentOf>
    <InferenceStep>
      <hasInferenceEngine rdf:resource="http://inference-web.org/registry/IE/SWIPL.owl#SWIPL"/>
      <hasInferenceRule rdf:resource="http://inference-web.org/registry/DPR/Hyp-Resolution.owl#Hyp-Resolution"/>
      <hasAntecedentList>
      <NodeSetList>
      <ds:first rdf:resource="https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_2"/>
      <ds:rest>
      <NodeSetList>
      <ds:first rdf:resource="https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_3"/>
      </NodeSetList>
      </ds:rest>
      </NodeSetList>
      </hasAntecedentList>
    </InferenceStep>

Justification 2* Using Prolog's Hyper Resolution, we have the proof:

[isCool(X) :- isPopular(X); isComputerScientist(X)] and [isComputerScientist(nick)]
-----------------------------------------------------------------------------------
                     [isCool(nick)]

This part of the proof is encoded by the RDF/XML below:

  </isConsequentOf>
  <isConsequentOf>
    <InferenceStep>
      <hasInferenceEngine rdf:resource="http://inference-web.org/registry/IE/SWIPL.owl#SWIPL"/>
      <hasInferenceRule rdf:resource="http://inference-web.org/registry/DPR/Hyp-Resolution.owl#Hyp-Resolution"/>
      <hasAntecedentList>
      <NodeSetList>
      <ds:first rdf:resource="https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_2"/>
      <ds:rest>
      <NodeSetList>
      <ds:first rdf:resource="https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_9"/>
      </NodeSetList>
      </ds:rest>
      </NodeSetList>
      </hasAntecedentList>
    </InferenceStep>
  </isConsequentOf>