CWM- PML1 Translation

Table of Contents

1. Required Resources
2. Trasnlation from CWM Proof Dump to PML
1. CWM Reason Ontology
2. PML Ontology
3. Translation Rules
   
3. Translation Examples
1. Socreates
2. Witch
3. Vegterian
   
4. Change Log
   

1. Required Resources

2. Trasnlation from CWM Proof Dump to PML 

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 2.1: Structure of Reason ontology.

• 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   { ...}

2.2. 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 2.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.

• 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  {...}

2.3 Translation 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. Translation Examples

3.1 Socreates

3.2 Witch

3.3 Vegetarian

4. Change Log

• 8:39 AM 2/8/2007:  this document is created. 
• Examples are provided by  Dan Connonly 
• translation rules is authored by Lalana Kagal and Li Ding.
• section 2 is adapted from an earlier document  http://iw.stanford.edu/2006/tami/