N3 SEM proof for simple test case using e:disjunction -- in 21 msec

GIVEN -- http://eulersharp.sourceforge.net/2007/07test/socrates.n3
+++++

--8<--
:socrates a :Human.
:socrates a :NonFemale.

:NonFemale owl:disjointWith :Female.
:Human rdfs:subClassOf :MaleOrFemale.
:MaleOrFemale owl:unionOf (:Female :Male).
:Female rdfs:subClassOf :Mortal.
:Male rdfs:subClassOf :Mortal.


### RDF plus OWL support

{?X a ?Y. ?Y rdfs:subClassOf ?Z} => {?X a ?Z}.

{?X a ?Y. ?Y owl:disjointWith ?Z. ?X a ?Z} => false.

{?I a ?X. ?X rdfs:subClassOf ?Y. ?Y owl:unionOf (?A ?B)} => ({?I a ?A} {?I 
a ?B})!e:disjunction.
{?I a ?X. ?X rdfs:subClassOf ?Y. ?Y owl:unionOf (?A ?B ?C)} => ({?I a ?A} 
{?I a ?B} {?I a ?C})!e:disjunction.
--8<--


QUERY -- http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3
+++++

--8<--
{?X a ?Y} => {?X a ?Y}.
--8<--


PROOF -- http://eulersharp.sourceforge.net/2007/07test/socratesE.n3
+++++

--8<--
[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Human}; r:evidence (
  [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; 
r:source nsp0:pos_364_line_8]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :Human.}].

[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :NonFemale}; r:evidence 
(
  [ a r:Extraction; r:gives {:socrates a :NonFemale}; r:because [ a 
r:Parsing; r:source nsp0:pos_384_line_9]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :NonFemale.}].

[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :MaleOrFemale}; 
r:evidence (
  [ a r:Inference; r:gives {:socrates a :MaleOrFemale}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a 
r:Parsing; r:source nsp0:pos_364_line_8]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; 
r:because [ a r:Parsing; r:source nsp0:pos_443_line_12]]);
   r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_611_line_20]]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :MaleOrFemale.}].

[ e:falseModel {:socrates a :Female}
; e:because [ e:integrityConstraint {{:socrates a :NonFemale. :NonFemale 
owl:disjointWith :Female. :socrates a :Female} => false}
  ; e:selected [ e:triple {:socrates a :NonFemale}
    ; e:falseAncestors {}
    ; e:falseDecendents {}
    ; e:consistentGives {:socrates a :Human. :NonFemale owl:disjointWith 
:Female. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf 
(:Female :Male). :Female rdfs:subClassOf :Mortal. :Male rdfs:subClassOf 
:Mortal. :socrates a :MaleOrFemale. :socrates a :Female. :socrates a 
:Mortal}
    ]
  ; e:selected [ e:triple {:NonFemale owl:disjointWith :Female}
    ; e:falseAncestors {}
    ; e:falseDecendents {}
    ; e:consistentGives {:socrates a :Human. :socrates a :NonFemale. 
:Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female 
:Male). :Female rdfs:subClassOf :Mortal. :Male rdfs:subClassOf :Mortal. 
:socrates a :MaleOrFemale. :socrates a :Female. :socrates a :Mortal}
    ]
  ; e:selected [ e:triple {:socrates a :Female}
    ; e:falseAncestors {}
    ; e:falseDecendents {}
    ; e:consistentGives {:socrates a :Human. :socrates a :NonFemale. 
:NonFemale owl:disjointWith :Female. :Human rdfs:subClassOf :MaleOrFemale. 
:MaleOrFemale owl:unionOf (:Female :Male). :Female rdfs:subClassOf 
:Mortal. :Male rdfs:subClassOf :Mortal. :socrates a :MaleOrFemale}
    ]
  ]
; r:gives {
[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a 
r:Parsing; r:source nsp0:pos_364_line_8]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; 
r:because [ a r:Parsing; r:source nsp0:pos_443_line_12]]
   [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; 
r:because [ a r:Parsing; r:source nsp0:pos_488_line_13]]);
   r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_713_line_24]]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :Female.}].

[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
   [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
    [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a 
r:Parsing; r:source nsp0:pos_364_line_8]]
    [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; 
r:because [ a r:Parsing; r:source nsp0:pos_443_line_12]]
    [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; 
r:because [ a r:Parsing; r:source nsp0:pos_488_line_13]]);
    r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_713_line_24]]]
   [ a r:Extraction; r:gives {:Female rdfs:subClassOf :Mortal}; r:because 
[ a r:Parsing; r:source nsp0:pos_525_line_14]]);
   r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_611_line_20]]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :Mortal.}].

}].

[ e:possibleModel {:socrates a :Male}
; r:gives {
[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a 
r:Parsing; r:source nsp0:pos_364_line_8]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; 
r:because [ a r:Parsing; r:source nsp0:pos_443_line_12]]
   [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; 
r:because [ a r:Parsing; r:source nsp0:pos_488_line_13]]);
   r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_713_line_24]]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :Male.}].

[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
   [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
    [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a 
r:Parsing; r:source nsp0:pos_364_line_8]]
    [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; 
r:because [ a r:Parsing; r:source nsp0:pos_443_line_12]]
    [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; 
r:because [ a r:Parsing; r:source nsp0:pos_488_line_13]]);
    r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_713_line_24]]]
   [ a r:Extraction; r:gives {:Male rdfs:subClassOf :Mortal}; r:because [ 
a r:Parsing; r:source nsp0:pos_556_line_15]]);
   r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp0:pos_611_line_20]]]);
  r:rule [ a r:Extraction; r:because [ a r:Parsing; r:source 
nsp1:pos_728_line_11]]];
 r:gives {
  :socrates a :Mortal.}].

}].

#ENDS 21 msec.
--8<--


README -- http://eulersharp.sourceforge.net/README plus 
http://eulersharp.sourceforge.net/GUIDE


Kind Regards,

Jos De Roo | Agfa HealthCare
Senior Researcher | HE/Advanced Clinical Applications Research
T  +32 3444 6256

Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
http://www.agfa.com/healthcare/
R.O.: Septestraat 27, B-2640 Mortsel, Belgium | RLE Antwerp | VAT BE 
0403.003.524 | IBAN BE03570124715584 | Citibank International PLC, B-1050 
Brussels
Click on link to read important disclaimer: 
http://www.agfa.com/healthcare/maildisclaimer