Skolem Euler Machine

The notation that is used is N3[1] and the logic is N3Logic[2].
N3 builtins are described in CwmBuiltins[3] and log-rules[4].

The toolchain is

        N3 data/proof output

                /\
               /||\ sem.pl
                ||

        Prolog Coherent Logic

                /\
               /||\ EulerRunner.java
                ||

        N3 data/rules input


Some SEM test cases and results

Euler5 proof engine

The notation that is used is N3[1] and the logic is N3Logic[2].

N3 builtins are described in CwmBuiltins[3] and log-rules[4] and
to model truth-conditions the following predicate is used

e:true a rdf:Property;
        rdfs:domain rdfs:Resource;
        rdfs:range xsd:decimal;
        rdfs:comment """builtin to model truth-value t(conclusion|premises)""".

Another predicate (which is not a builtin) that is typically used
to model the truth-value of logical propositions is

e:boolean a rdf:Property;
        rdfs:domain rdfs:Resource;
        rdfs:range [ owl:oneOf (e:T e:F)];
        rdfs:comment """to model a logical proposition""".

The modeling is done in the form of t-rules and the semantics of

{P e:boolean e:T. Q e:boolean e:T. _: e:true x} => {C e:boolean e:T}.

is t(C|P,Q) = x.

If the conclusion of a t-rule is e:boolean e.g.

{:P e:boolean e:T. _: e:true 0.2} => {:C e:boolean e:T}.

then we should add the t-rule

{:P e:boolean e:T. _: e:true 0.8} => {:C e:boolean e:F}.

because if t(C|P) = x then t(~C|P) = 1-x.

In the logical case i.e. when x = 1 this amounts to
saying C iftrue P which avoids the "ex falso quodlibet".

The query answers are obtained via proof interpretation implemented as
in euler.pl[5] and the detailed model theory is under investigation.

The proof engine runs as an euler --prolog-bchain --nefq service
which is declared in codd.properties[6].

Euler5 prover is based on

  Horn Logic[8]
  + chaining enhanced with Euler path detection (lemma case and fail case)
  + equality as substitution of equals by equals
  + scoped negation and scoped aggregation (findall)
  + functions as builtin predicates with a subject or object list

  Bayes Rule[9]
  + t-rules using e:true predicate
  + t-rulesets can be incomplete, redundant and with loops

Test case

RULES http://eulersharp.sourceforge.net/2004/04test/socratesP.n3

:Socrates a :Man.
:Man rdfs:subClassOf :Mortal.

{?A rdfs:subClassOf ?B. ?S a ?A} => {?S a ?B}.


QUERY http://eulersharp.sourceforge.net/2004/04test/socratesQ.n3

{?WHO a ?WHAT} => {?WHO a ?WHAT}.


PROOF http://eulersharp.sourceforge.net/2004/04test/socratesR.n3

[ a r:Proof, r:Conjunction;
  r:component [ a r:Inference; r:gives {:Socrates rdf:type :Man}; r:evidence (
    [ a r:Extraction; r:gives {:Socrates rdf:type :Man}; r:because [ a r:Parsing;
      r:source <http://eulersharp.sourceforge.net/2004/04test/socratesP.n3>]]);
    r:binding [ r:variable [ n3:uri "http://localhost/var#WHO"]; r:boundTo [
      n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Socrates"]]; 
    r:binding [ r:variable [ n3:uri "http://localhost/var#WHAT"]; r:boundTo [
      n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Man"]]; 
    r:rule [ a r:Extraction; r:gives {@forAll var:WHO,var:WHAT.
      {var:WHO a var:WHAT} => {var:WHO a var:WHAT}. }; r:because [ a r:Parsing;
      r:source <http://eulersharp.sourceforge.net/2004/04test/socratesQ.n3>]]];
  r:component [ a r:Inference; r:gives {:Socrates rdf:type :Mortal}; r:evidence (
    [ a r:Extraction; r:gives {:Socrates rdf:type :Mortal}; r:because [ a r:Inference;
      r:gives {:Socrates rdf:type :Mortal}; r:evidence (
      [ a r:Extraction; r:gives {:Man rdfs:subClassOf :Mortal}; r:because [ a r:Parsing;
        r:source <http://eulersharp.sourceforge.net/2004/04test/socratesP.n3>]]
      [ a r:Extraction; r:gives {:Socrates rdf:type :Man}; r:because [ a r:Parsing;
        r:source <http://eulersharp.sourceforge.net/2004/04test/socratesP.n3>]]);
      r:binding [ r:variable [ n3:uri "http://localhost/var#A"]; r:boundTo [
        n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Man"]]; 
      r:binding [ r:variable [ n3:uri "http://localhost/var#B"]; r:boundTo [
        n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Mortal"]]; 
      r:binding [ r:variable [ n3:uri "http://localhost/var#S"]; r:boundTo [
        n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Socrates"]]; 
      r:rule [ a r:Extraction; r:gives {@forAll var:A,var:B,var:S.
        {var:A rdfs:subClassOf var:B. var:S a var:A} => {var:S a var:B}. };
        r:because [ a r:Parsing;
        r:source <http://eulersharp.sourceforge.net/2004/04test/socratesP.n3>]]]]);
    r:binding [ r:variable [ n3:uri "http://localhost/var#WHO"]; r:boundTo [
      n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Socrates"]]; 
    r:binding [ r:variable [ n3:uri "http://localhost/var#WHAT"]; r:boundTo [
      n3:uri "http://eulersharp.sourceforge.net/2004/04test/socrates#Mortal"]]; 
    r:rule [ a r:Extraction; r:gives {@forAll var:WHO,var:WHAT.
      {var:WHO a var:WHAT} => {var:WHO a var:WHAT}. }; r:because [ a r:Parsing;
      r:source <http://eulersharp.sourceforge.net/2004/04test/socratesQ.n3>]]];
  r:gives {
    :Socrates rdf:type :Man.
    :Socrates rdf:type :Mortal.}].

Test case using t-rules

RULES http://eulersharp.sourceforge.net/2004/04test/metastaticP.n3

{_: e:true 0.2} => {:MetastaticCancer e:boolean e:T}.

{:MetastaticCancer e:boolean e:T. _: e:true 0.8} => {:SerumCalcium e:boolean e:T}.
{:MetastaticCancer e:boolean e:F. _: e:true 0.2} => {:SerumCalcium e:boolean e:T}.

{:MetastaticCancer e:boolean e:T. _: e:true 0.2} => {:BrainTumor e:boolean e:T}.
{:MetastaticCancer e:boolean e:F. _: e:true 0.05} => {:BrainTumor e:boolean e:T}.

{:SerumCalcium e:boolean e:T. :BrainTumor e:boolean e:T. _: e:true 0.8}
        => {:Coma e:boolean e:T}.
{:SerumCalcium e:boolean e:T. :BrainTumor e:boolean e:F. _: e:true 0.8}
        => {:Coma e:boolean e:T}.
{:SerumCalcium e:boolean e:F. :BrainTumor e:boolean e:T. _: e:true 0.8}
        => {:Coma e:boolean e:T}.
{:SerumCalcium e:boolean e:F. :BrainTumor e:boolean e:F. _: e:true 0.05}
        => {:Coma e:boolean e:T}.

{:BrainTumor e:boolean e:T. _: e:true 0.8} => {:HeadAche e:boolean e:T}.
{:BrainTumor e:boolean e:F. _: e:true 0.6} => {:HeadAche e:boolean e:T}.


QUERY http://eulersharp.sourceforge.net/2004/04test/metastaticQ.n3

{:Coma e:boolean e:F. :HeadAche e:boolean e:T} => {:MetastaticCancer e:boolean e:T}.


PROOF http://eulersharp.sourceforge.net/2004/04test/metastaticR.n3

[ e:proofID 1; e:proof {
        {:Coma e:boolean e:F} e:because {
                {:SerumCalcium e:boolean e:T} e:because {
                        {:MetastaticCancer e:boolean e:T} e:because {
                                {var:_G561 e:true 0.2} a e:Builtin.
                                }; e:source nsp0:pos_180_line_4.
                        {var:_G571 e:true 0.8} a e:Builtin.
                        }; e:source nsp0:pos_264_line_6.
                {:BrainTumor e:boolean e:T} e:because {
                        {:MetastaticCancer e:boolean e:T} a e:Lemma.
                        {var:_G600 e:true 0.2} a e:Builtin.
                        }; e:source nsp0:pos_429_line_9.
                {(1.0 0.8) math:difference 0.2} a e:Builtin.
                {var:_G637 e:true 0.2} a e:Builtin.
                }; e:source nsp0:pos_610_line_12.
        {:HeadAche e:boolean e:T} e:because {
                {:BrainTumor e:boolean e:T} a e:Lemma.
                {var:_G666 e:true 0.8} a e:Builtin.
                }; e:source nsp0:pos_979_line_17.
        {:MetastaticCancer e:boolean e:T} a e:Lemma.
        }; e:possibility 0.00512].

[ ... ]

[ e:bayesRule ((1 3 5 7) (9 10 11 12 13 14 15 16)); r:gives {
        {:Coma e:boolean e:F. :HeadAche e:boolean e:T. _: e:true 0.0972762645914397}
                => {:MetastaticCancer e:boolean e:T}}].

[ e:bayesRule ((2 4 6 8) (9 10 11 12 13 14 15 16)); r:gives {
        {:Coma e:boolean e:F. :HeadAche e:boolean e:T. _: e:true 0.90272373540856}
                => {:MetastaticCancer e:boolean e:F}}].

Delta analysis

RULES http://eulersharp.sourceforge.net/2007/07test/irP.n3

### incomplete and redundant belief rules

{_: e:true 0.15} => {:P e:boolean e:T}.

{_: e:true 0.35} => {:Q e:boolean e:T}.

{:P e:boolean e:T. _: e:true 0.66} => {:C e:boolean e:T}.
#{:P e:boolean e:F. _: e:true 0.42} => {:C e:boolean e:T}.

{:Q e:boolean e:T. _: e:true 0.84} => {:C e:boolean e:T}.
{:Q e:boolean e:F. _: e:true 0.74} => {:C e:boolean e:T}.
{:Q e:boolean e:F. _: e:true 0.63} => {:C e:boolean e:T}.

{:P e:boolean e:T} => {:Q e:boolean e:T}.

### with loops and calculated belief
{:C e:boolean e:T. (0.98 0.98) math:product ?B. _: e:true ?B} => {:P e:boolean e:T}.
{:C e:boolean e:F. _: e:true 0.86} => {:P e:boolean e:T}.


QUERY http://eulersharp.sourceforge.net/2007/07test/irQ.n3

{:C e:boolean e:T} => {?X e:boolean ?Y}.


PROOF http://eulersharp.sourceforge.net/2007/07test/irR.n3

[ ... ]

(16 25) e:delta 0.010725.                         # between proofs ( )
(17 26) e:delta 0.060775.
(18 27) e:delta 0.0715.
(19 28) e:delta 0.0715.
(20 29) e:delta 0.0686685999999999.
(21 30) e:delta 0.0028314.
(34 36) e:delta 0.0715.

((2) (5)) e:delta 0.06435.                        # between models (( ))
((3) (6)) e:delta 0.06435.
((4) (10 19)) e:delta 0.676.
((8 17) (12 21)) e:delta 0.62806.

(((8 17) (32 34)) ((1) (31))) e:delta 0.85.       # between theories ((( )))
(((1) (31)) ((8 17) (32 34))) e:delta 0.85.
(((1) (31)) ((12 21) (32 34))) e:delta 0.0396000000000001.

Using SQL and XML

To cope with large amounts of triples, one can use euler --sql
to translate triples into SQL and after adding e.g.

dbname.driver               = org.sqlite.JDBC
dbname.uri                  = jdbc:sqlite:tripleStore/dbname

to codd.properties[6] one can get e.g.

http://host.domain/dbname?SQL=sql where sql is an urlencoding of e.g.

SELECT '@prefix ', prefix, ' ', namespace, '.' FROM pfx;
SELECT '';
SELECT subject, ' ', predicate, ' ', object, '.' FROM rdf
  WHERE predicate == 'rdfs:subClassOf' AND object == ':Event';


Similar queries can be used to get triples out of the huge amount
of existing relational data. For instance, given a database table
tbl1 with columns one and two the following query result is a set
of RDF/N3 triples

SELECT '@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.';
SELECT '@prefix : <http://www.agfa.com/w3c/euler/dtP#>.';
SELECT '';
SELECT '"', one, '" :birthday "', two, '"^^xsd:gYear.' FROM tbl1
  WHERE two == 1956;


To get triples from any xml serialization one can use xml2sql[10]
i.e. after running the database create script

echo "BEGIN TRANSACTION;" > ${1}.sql
echo "create table t_xmltosql_ent" >> ${1}.sql
echo " (c_id char(8), c_nr integer, c_depth integer, c_ent integer," >> ${1}.sql
echo " c_tag char(30), c_val text, primary key (c_id, c_nr));" >> ${1}.sql
echo "create table t_xmltosql_att" >> ${1}.sql
echo " (c_id char(8), c_nr integer, c_ent integer, c_att char(30)," >> ${1}.sql
echo " c_val text, primary key (c_id, c_nr));" >> ${1}.sql
cat "${1}.xml"| latin1-utf8| entityfix| xml2sql-v -a "'${1}'"| utf8-latin1 >> ${1}.sql
echo "COMMIT;" >> ${1}.sql
rm -fr ${1}
sqlite3 -init ${1}.sql ${1}

one can pose an SQL query to get the desired triples as a resultset.

T-rules model theory

Given truth-value function t and boolean decision/support variables X and Y

t(X,Y) = t(X|Y)*t(Y)                               [A1]

t(X,Y) = t(Y,X)                                    [A2]

t(X;Y) = t(X)+t(Y)-t(X,Y)                          [A3]

t(X;~X) = 1                                        [A4]

t(~X) = 1-t(X)                                     [A5]


t(X|Y) = t(Y,X)/t(Y)
       = t(Y|X)*t(X)/t(Y)                          [T1] [Bayes theorem]

t(X|Y) = (t(~Y;X)-t(~Y))/t(Y)
         is undefined when Y is the empty set F    [T2] [no "ex falso quodlibet"]


Additional semantic constraints are:

        IF                     | THEN
        -----------------------|---------------
        X independent from Y   | t(X|Y) = t(X)
            Y universal set T  | t(X|T) = t(X)
        X dependent from Y     | t(X|Y) != t(X)
            Y subset of X      | t(X|Y) = 1
            Y disjoint from X  | t(X|Y) = 0


For the graph

         p = t(X) .---. s = t(Y|X)  .---. q = t(Y)
        --------->| X |------------>| Y |<---------
                  '---' a = t(Y|~X) '---'

it is the case that

        q = p*s+(1-p)*a

        a = (q-p*s)/(1-p)

        s = (q-(1-p)*a)/p

        p = (q-a)/(s-a)

References

 [1] http://www.w3.org/TeamSubmission/n3/
 [2] http://www.w3.org/DesignIssues/N3Logic
 [3] http://www.w3.org/2000/10/swap/doc/CwmBuiltins
 [4] http://eulersharp.sourceforge.net/2003/03swap/log-rules.n3
 [5] http://eulersharp.sourceforge.net/2006/02swap/euler.pl
 [6] http://eulersharp.sourceforge.net/2004/01swap/codd.properties
 [7] http://eulersharp.sourceforge.net/
 [8] http://en.wikipedia.org/wiki/Horn_logic
 [9] http://en.wikipedia.org/wiki/Bayes_Rule
[10] http://www.scylla-charybdis.com/tools.html


Jos De Roo
$Id: GUIDE 2064 2008-05-01 13:45:05Z josd $