Euler Proof Mechanism

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.

Euler Abstract Machine (EAM)

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

Euler under the hood

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 P-code (N3P)

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>.

Using SQL

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=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;

Belief calculus model theory

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)

End

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