Euler Yet another proof Engine - EYE
EYE is a reasoning engine supporting the Semantic Web layers.
It performs forward and backward chaining along Euler paths.
Via N3 it is interoperable with Cwm.
Forward chaining is applied for rules using => in N3 and backward chaining
is applied for rules using <= in N3 which one can imagine as built-ins.
Euler paths are roughly "don't step in your own steps" which is inspired by
what Leonhard Euler discovered in 1736 for the Königsberg Bridge Problem.
EYE sees the rule P => C as P & ˜C => C.
Architecture and design
The EYE stack comprises the following Software and Machines:
This is what the basic EAM (Euler Abstract Machine) does in a nutshell:
- Select rule
P => C
- Prove
P & ˜C (backward chaining) and if it fails backtrack to 1.
- If
P & ˜C assert C (forward chaining) and remove brake
- If
C = answer(A) and tactic limited-answer stop, else backtrack to 2.
- If brake or tactic linear-select stop, else start again at 1.
EYE Unifying Logic
EYE Reasoning
Running the Semantic Web Databus and Proofbus from Tim Berners-Lee which is
like a world wide welding machine transforming data into proofs:
Examples and Test Cases
- bayesian networks:
ccd,
nbbn,
swet
- control systems:
cs
- description logic:
bmt,
dt,
edt,
entail,
gedcom,
graph,
h2o,
RDF plus OWL
(source)
- ershovian compilation:
preduction
- extensible imaging:
lldm
- logic programming:
4color,
disjunction-elimination,
dp,
diamond-property,
gcc,
hanoi,
lee,
socrates,
witch,
zebra
- markovian networks:
mmln
- mathematical reasoning:
fibonacci,
padovan,
pi,
polygon,
tak
- neural networks:
fcm,
fgcm
- quantum computation:
dqc
- universal machines:
turing,
usm
- workflow composers:
gps,
map,
resto,
restpath,
twf
See also