GUIDE (original) (raw)

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 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 => and the object of e:tactic is a list containing and . For every reasoning step there is a which is initially the empty list. Input clauses that have an e:tactic are only selected when their unifies with the and when the input clause can be satisfied becomes .

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 9856 2020-01-04 19:22:22Z josd $