Euler Yet another proof Engine - EYE

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:

  1. Select rule P => C
  2. Prove P & ˜C (backward chaining) and if it fails backtrack to 1.
  3. If P & ˜C assert C (forward chaining) and remove brake
  4. If C = answer(A) and tactic limited-answer stop, else backtrack to 2.
  5. 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

See also