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

Some more background as we should be as explicit as possible..


As engineers we all too often assume an "all knowledge is contained in 
here"
which is of course never working out. By dropping this assumption for 
ever,
the Semantic Web gives us a means to achieve a fresh "Socratic 
Completeness":

  To solve a problem, it would be broken down into a series of questions,
  the answers to which gradually distill the answer you seek -- Socrates


Having running code and simple test cases is a practical way to tackle
real world problems. This has to go hand in hand with a sharp theoretical
foundation based on classical logic which is all we need because:

  The property of formal derivability is semidecidable: there is an 
algorithm
  by means of which, if a sentence S is in fact formally derivable from a
  sentence P, then this fact can be mechanically detected -- John Alan 
Robinson


In our Semantic Web applications we actually use N3 as the "legislation"
language, the JVM as an "execution" platform and Euler SEM as a 
"reasoning"
engine which is open sourced at http://eulersharp.sourceforge.net/


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



Jos De Roo/AMDUS/AGFA 
08/14/2008 11:43 PM

To
www-archive@w3.org
cc

Subject
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