# USAGE: c

@keywords a, is, of.

# Rules to take a proof as emitted by cwm into a proof as input by InferenceWeb
#

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix crypto: <http://www.w3.org/2000/10/swap/crypto#> .
@prefix string: <http://www.w3.org/2000/10/swap/string#> .
@prefix os: <http://www.w3.org/2000/10/swap/os#> .
@prefix list: <http://www.w3.org/2000/10/swap/list#>.

@prefix rea: <http://www.w3.org/2000/10/swap/reason#> .
@prefix n3: <http://www.w3.org/2004/06/rei#> .
@prefix iw: <http://inferenceweb.stanford.edu/2004/07/iw.owl#> .

@prefix s: <http://www.w3.org/2000/01/rdf-schema#> .

@prefix time: <http://www.w3.org/2000/10/swap/time#> .
@prefix dt: <http://www.w3.org/2001/XMLSchema#>.

# Translation rules (much could be done with OWL but we have rules)
{ ?S a [ s:subClassOf ?C] } => { ?S a ?C}. # a bit of RDFS

# make up a nearby URI
{ ?S a [ s:subClassOf rea:Step] } => { ?S aux [] }.

{ ?S aux [ log:rawUri ?I ].
 (?I "[^#]#(.*)") string:search (?FRAG).
  ?X log:uri ("#ns_" ?FRAG).string:concatenation.os:baseAbsolute.
  ?C log:uri ("#is_" ?FRAG).string:concatenation.os:baseAbsolute.
} => { ?C a iw:InferenceStep; iw:hasInferenceEngine <http://inferenceweb.stanford.edu/registry/IE/CWM.owl#CWM>.
       ?X a iw:NodeSet; rea:step ?S; iw:isConsequentOf ?C }.

{ ?S a rea:Proof.
  ?NODESET rea:step ?S
} => { ?NODESET rea:step rea:Proof }.


#### gives 

# special handling for conjunction because every nodeset has to have a conclusion
# will be fixed
{ ?X a rea:Conjunction; rea:component ?Y.
  ?X rea:gives ?G.
 } => { ?Y rea:gives ?G }.

{ ?NODESET iw:isConsequentOf ?C; rea:step ?S.
  ?S rea:gives ?Y.
  ?Y log:n3String ?str.
} => { ?NODESET iw:hasConclusion ?str; iw:hasLanguage n3:N3 }.

#### Parsing step 
{ ?S a rea:Extraction; rea:because ?X.
  ?X a rea:Parsing; rea:source ?Y.
  ?NODESET rea:step ?S; iw:isConsequentOf ?C.
  "" time:localTime ?NOW.
  (?NOW dt:dateTime) log:dtlit ?NOW_T.
 } => { ?C iw:hasSourceUsage [
   a iw:SourceUsage;
   iw:hasSource ?Y;
   iw:usageTime ?NOW_T
  ] }.

{ ?S a rea:Extraction; rea:because ?X; rea:gives ?G.
  ?X a rea:Inference.
  ?G log:n3String ?str.
  ?NODESET1 rea:step ?S; iw:isConsequentOf ?C1.
  ?NODESET2 rea:step ?X.
} => { ?C1 iw:hasAntecedent ?NODESET2. ?NODESET2 iw:hasConclusion ?str; iw:hasLanguage n3:N3 }.

### Extraction step
{ ?NODESET iw:isConsequentOf ?C; rea:step ?S.
   ?S a rea:Extraction
} => { ?C iw:hasRule <http://inferenceweb.stanford.edu/registry/DPR/Extraction.owl#Extraction> }.


### Conjunction step 
{ ?X a rea:Conjunction; rea:component ?Y.
  ?NODESET1 rea:step ?X; iw:isConsequentOf ?C1.
  ?NODESET2 rea:step ?Y.
 } => { ?C1 iw:hasRule <http://inferenceweb.stanford.edu/registry/DPR/Conjunction.owl#Conjunction>;
     iw:hasAntecedent ?NODESET2 }.


### Inference step

{ ?X a rea:Inference.
  ?NODESET rea:step ?X; iw:isConsequentOf ?C.
} => { ?C iw:hasRule <http://inferenceweb.stanford.edu/registry/DPR/Inference.owl#Inference> }.

{ ?X a rea:Inference;
     rea:binding [
            rea:variable  [n3:uri ?var ];
            rea:boundTo  [ n3:uri ?val ]]. #@@can be bound to bnodes too. hmm.
  ?NODESET rea:step ?X; iw:isConsequentOf ?C.
} => { ?C iw:hasVariableMapping [
                                    a iw:Mapping;
                                    iw:mapFrom  ?var; iw:mapTo ?val ] }.

{ ?X rea:evidence [ is list:in of ?Y].
  ?NODESET1 rea:step ?X; iw:isConsequentOf ?C1.
  ?NODESET2 rea:step ?Y.
} => { ?C1  iw:hasAntecedent ?NODESET2 }.

{ ?X rea:rule ?Y.
  ?NODESET1 rea:step ?X; iw:isConsequentOf ?C1.
  ?NODESET2 rea:step ?Y.
} => { ?C1  iw:hasAntecedent ?NODESET2 }.


#ends