Euler is an inference engine supporting logic based proofs. It is a backward-forward-backward chaining reasoner enhanced with Euler path detection. The backward-forward-backward chaining is realized via an underlying Prolog backward chaining, a forward meta-level reasoning and a backward proof construction. The Euler path detection is roughly "don't step in your own steps" to avoid vicious circles so to speak and in that respect there is a similarity with what Leonhard Euler discovered in 1736 for the Königsberg Bridge Problem. Via N3 the reasoner is interoperable with W3C Cwm. See also README and the software is maintained at EulerSharp.

The notation that is used is N3 and the logic is N3Logic. N3 builtins are described in CwmBuiltins and log-rules. Internally EAM is using Notation 3 P-code (N3P) which is an intermediate code: N3 data/proof output /\ /||\ || N3 P-code (N3P) /\ /||\ || N3 data/rules input Some test cases and results

Things are layered and cascaded as follows: .------------------. .------------|- - - N3S | | N3P |-----'------------| |------------|- - -' EAM | | PVM |-----'------------| |------------|- - -' WAM | | ASM |-----'------------| '------------|- - -' CPU | '------------------' Legend ------ N3S = Notation 3 Socket N3P = Notation 3 P-code EAM = Euler Abstract Machine PVM = Prolog Virtual Machine code WAM = Warren Abstract Machine ASM = Assembly code CPU = Central Processing Unit For proof tactics the main idea is to annotate the original N3 formulae instead of tampering with them. That way proof tactics can even be derived on the fly using N3 rules. Euler is making use of builtins to support the eam/n engines: \/ \ o answers \/ \/ eam/3 engine \ o / \/ / || \/ \||/ || \/ eam/1 engine || || --------------------||----- data ----- /\ builtins / \ /\

N3 formulae are translated in N3 P-code input clauses of the form implies(<conjunction>,<disjunction>,<src>). All the variables used in <conjunction> are universally quantified and all the other variables are existentially quantified. Variables start with an upper case letter or the '_' character. The conjunction operator is ',' and the disjunction operator is ';'. Comments start with '%' and end with the next end of line. Proof tactics can be declared in N3LOGIC with the binary predicate {<conjunction> => <disjunction>} e:tactic (<guard> <new_guard>). The subject of e:tactic is an instance of <conjunction> => <disjunction> and the object of e:tactic is a list containing <guard> and <new_guard>. For every reasoning step there is a <current_guard> which is initially the empty list. Input clauses that have an e:tactic are only selected when their <guard> unifies with the <current_guard> and when the input clause can be satisfied <current_guard> becomes <new_guard>.

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 one can get e.g.http://host.domain/dbname?SQL=sqlwhere 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;

Given truth-value function t and boolean decision/support variables X and Y t(X,Y) = t(X|Y)*t(Y) [A1] [conjunction] t(X,Y) = t(Y,X) [A2] [commutativity] t(X;Y) = t(X)+t(Y)-t(X,Y) [A3] [disjunction] t(X;~X) = 1 [A4] [complement] t(~X) = 1-t(X) [A5] [negation] 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"] t(X) = t(X,Y)+t(X,~Y) [T3] [total belief theorem] t(~X,~Y) = t(~(X;Y)) [T4] [De Morgan theorem 1] t(~X;~Y) = t(~(X,Y)) [T5] [De Morgan theorem 2] 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)

Jos De Roo$Id: GUIDE 6259 2013-05-14 20:21:23Z josd $