Euler proof engine GUIDE -- Jos De Roo

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 belief the following predicate is used

e:true a rdf:Property;
	rdfs:domain rdfs:Resource; rdfs:range xsd:decimal;
	rdfs:comment """builtin to always succeed""".

Another predicate (which is not a builtin) that is typically used to
model belief 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 "belief rules" and the semantics of

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

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

If the conclusion of a belief 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 belief rule

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

because if belief(C|P) = x then belief(~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.yap[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] and is implemented[7] as

                       REST/N3
                .------------------.      .---.
                |     EulerLib     | <-> |'---'|
                |                  | SQL |     |
                |  Bayes    Horn   |     |     |
                |  Rule     Logic  |      '---'
                '------------------'

EulerLib is built on top of

  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]
  + belief rules using e:true predicate
  + belief rulesets can be incomplete, redundant and with loops
  + for sub models select minimal model
    for same models select model with maximum entropy
    for same models with same entropy select maximum belief/minimum disbelief

A typical test case is

RULES http://eulersharp.sourceforge.net/2004/04test/metastaticP.n3
QUERY http://eulersharp.sourceforge.net/2004/04test/metastaticQ.n3
PROOF http://eulersharp.sourceforge.net/2004/04test/metastaticR.n3


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.


References
----------

 [1] http://www.w3.org/DesignIssues/Notation3
 [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.yap
 [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