Translating CWM Proof into PML

Working Draft

This version: 06/23/2006

Latest version: 

Editors:

Li Ding (ebiquity group, University of Maryland Baltimore County) 

Lalana Kagal,  CSAIL, MIT

Deborah L. McGuinness (Knowledge Systems Laboratory, Stanford University )

Paulo Pinheiro da Silva  (Knowledge Systems Laboratory, Stanford University)

Copyright ©2006 KSL and W3C

Abstract

Proof Markup Language (PML) helps users encode and share their proofs in RDF, and it is supported by a series of tools for generating, registering, searching, and visualizing the Proof content.  In order to expose CWM inference result in PML, we show how to translate a CWM inference dump (written in Reason ontology) to a PML document.

Table of contents

1. Introduction

...

2. Backgrounds

2.1 CWM reason ontology

The CWM's reason ontology ( http://www.w3.org/2000/10/swap/reason.n3 ) is used for representing the proofs generated by CWM. Figure 3.1 depicts the structure of  the reason ontology: the white-rectangles denote classes defined in reason ontology; the green-rectangles denote classes defined in other ontologies; the labels on arcs denotes the properties defined in reason ontology; and the arcs denote rdfs:domain and rdfs:range of the corresponding properties.

Step ( gives ) Proof Inference ( rule, evidence) Conjunction (component) Extraction (because) Parsing (source) CommandLine (args)   Binding(variable ,boundTo)

Figure 3.1: Structure of Reason ontology.

2.2 CWM Proof Generation

Now we use a simple example to show how CWM generate a proof encoded by reason ontology:

1. INPUT:  a N3 file containing some n3-facts and n3-rules: http://people.csail.mit.edu/lkagal/tami/example1.n3
2. INFERENCE: run the following command

   cwm http://people.csail.mit.edu/lkagal/tami/example1.n3 --think --filter="http://people.csail.mit.edu/lkagal/tami/example1.n3"

3. OUTPUT:  
   • inference result: http://people.csail.mit.edu/lkagal/tami/example1-think.n3
   • proof dump: http://people.csail.mit.edu/lkagal/tami/example1-proof.n3

2.3. PML Ontology

PML ontology helps encode justification trace (one justification trace may help users reconstruct several alternative proofs for an conclusion, which can be the answer of a iw:Query). Figure 3.2 depicts the semantic structure of PML ontology  and show how to organize a collection of iw:NodeSet to represent a justification trace.

Figure 3.2 Semantic Structure of PML ontology

A NodeSet represents a step in a proof whose conclusion is justified by any of the set of inference steps associated with the NodeSet. PML adopts the term ``node set'' since each instance of NodeSet can be viewed as a set of nodes gathered from one or more proof trees having the same conclusion.

• The URI  of a node set is the unique identifier of the node set. Every node set has exactly one well-formed URI.
• The Conclusion of a node set ( i.e., the object of iw:hasConclusion) represents the expression concluded by the proof step. Every node set has one conclusion, and a conclusion of a node set is of type Language.
• The Language of a node set is the language in which the conclusion is represented. Every node set has exactly one language, and that language is of type Language. Languages are in general registered in the IWRegistry.
• Each InferenceStep of a node set represents an application of an inference rule that justifies the node set's conclusion. Every node set has at least one inference step, and each inference step of a node set is of type InferenceStep.

An InferenceStep represents a justification for the conclusion of a node set. Inference steps are anonymous OWL classes defined within node sets. For this reason, it is assumed that applications handling PML proofs are able to identify the node set of a inference step. Also for this reason, inference steps have no URIs.

• The Rule of an inference step (i.e., the object of iw:hasRule) is the rule applied to produce the conclusion. Every inference step has one rule, and that rule is of type InferenceRule. Rules are in general registered in the IWRegistry by engine developers.
• The Antecedents of an inference step (i.e., the object of iw:hasAntecedent) is a collection of node sets each of whose conclusions is a premise of the application of the inference step's rule. The collection can contain any number of node sets including none. PML supports the order of premises in two folds:
  • The fact that the premises are ordered may be relevant for some rules such as ordered resolution that uses the order to match premises with the schemas of the associated rule. To this end, users may declare one iw:hasAntecedent that links to an instance of rdf:List, which is an ordered list of the antecedent node sets.
  • For other rules such as modus Ponens, the order of the premises is irrelevant; therefore, Antecedents can be viewed as a bag of premises. To this end, users may declar multiple iw:hasAntecedent each of which links to an antecedent node set. 
• Each VariableMapping of an inference step (i.e., the object of iw:hasVariableMapping)  is a mapping from a variable to a term specifying the substitutions performed on the premises before the application of the step's rule. An inference step can have any number of variable mappings including none, and each  variable mapping is of type Mapping. For instance, substitutions may be required to unify terms in premises in order to perform resolution.
• Each SourceUsage of an inference step (i.e., the object of iw:hasSourceUsage)  refers to the an entity representing where original statements from which the conclusion was obtained. It is always used with the "direct assertion" inference rule.  An inference step can have zero to one source usage,  and each source usage has exactly one source, whose type is Source, and a usage time (i.e., the object of iw:usageTime) indicating when the source has been used.
• The InferenceEngine of an inference step (i.e., the object of iw:hasInferenceEngine) is the inference engine that produced the inference step. Each inference step has one InferenceEngine, which is of type InferenceEngine. Inference engines are in general registered in the IWRegistry by engine developers.

3. Translation

3.1 Rules

Translating  instances of class

notes:

1. we have some discussions on differentiating pr:rule from pr:evidence. Someone (DanC?) also suggested un-ordered list. Do we still want that feature?
2. source:  the URL source should better be absolute URL

3.2 Example1

data sources:

• The knowledge base (represented in N3): http://people.csail.mit.edu/lkagal/tami/example1.n3
• The CWM proof dump: http://people.csail.mit.edu/lkagal/tami/example1-proof.n3
• The PML dump:

3.2.1 CWM dump structure analysis

Complete version: http://people.csail.mit.edu/lkagal/tami/example1-proof.n3 

• pr:Proof, pr:Conjunction   <URI>
  • pr:gives {...}
  • pr:component
    • pr:Inference
      • pr:binding
        • [ pr:variable …, pr:boundTo …]
        • [ pr:variable …, pr:boundTo …]
      • pr:evidence
        • pr:Extraction
          • pr:gives {...}
          • pr:because   <URI>
        • pr:Extraction
          • pr:gives {...}
          • pr:because   <URI>
        • pr:Extraction
          • pr:gives {...}
          • pr:because   <URI>
      • pr:rule
        • pr:Extraction
          • pr:gives {...}
          • pr:because <URI>     
• pr:Parsing
  • pr:because:  <URI>
  • pr:source:  <URL>
• pr:CommandLine <URI>
  • pr:args   { ...}

3.2.2 Brief PML Representation

Complete version:  http://iw.stanford.edu/doc/project/tami/example1-pml-0518.rdf     (View example1 in IW)

• iw:NodeSet rdf:id="g0"
  • iw:hasConclusion -- {...}
  • iw:hasLanguage --[[iwRegistry#N3]]
  • iw:isConsequentOf
    • iw:InferenceStep
      • iw:hasRule -- [[iwRegistry#CWM-Conjunction]]
      • iw:hasInferenceEngine -- [[iwRegistry#CWM]]
      • iw:hasAntecendent -- #g00
• iw:NodeSet rdf:id="g00"
  • iw:hasConclusion  --{...}
  • iw:hasLanguage --[[iwRegistry#N3]]
  • iw:isConsequentOf
    • iw:InferenceStep
      • iw:hasRule --[[iwRegistry#CWM-Inference]] (General Modus Ponens)
      • iw:hasInferenceEngine -- [[iwRegistry#CWM]]
      • iw:hasVariableMapping -- the first variable mapping
        • iw:Mapping
          • iw:mapFrom
          • iw:mapTo
      • iw:hasVariableMapping -- the second variable mapping
        • iw:Mapping
          • iw:mapFrom
          • iw:mapTo
      • iw:hasAntecendent -- parseType="Collection"
        • #g4  (an n3-rule)
        • #g1  (n3-fact1)
        • #g2  (n3-fact2)
        • #g3  (n3-fact3)
• iw:NodeSet -- (g1, g2, g3, g4 respectively)
  • iw:hasConclusion -- {...}
  • iw:hasLanguage -- [[iwRegistry#N3]]
  • iw:isConsequenceOf
    • iw:InferenceStep
      • iw:hasRule  [[iwRegistry#CWM-Extraction]] 
      • iw:hasInferenceEngine -- [[iwRegistry#CWM]]
      • iw:hasSourceUsage --
        • iw:SourceUsage
          • iw:hasSource  <src>
          • iw:usageTime
• iw:Source - - <src>   (we can help automatically register the source via HTTP request)
  • URL  {...}

Appendix A. Action Items

1. Find out whether hasSourceUsage can be used to link to the source documents (Li Ding)
2. reason.n3 does not contain info about evidence, rule, and args. Add those (Lalana)
3. Decide on mapping (Li and Lalana)
4. Figure out how to display more than one step in IW browser (Lalana)
5. Fix to-pml.n3 (Lalana)

Appendix B. Change Log

• May 30, 2006.   modified the description of reason ontology (Section 2.1, added rule, evidence, and args) including image. Update translation rule (reason:Extraction and reason:Parsing) 

last modified: 06/23/2006