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