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.
For examples and test cases see EYE Reasoning.

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 & NOT(C) => C.

Architecture and design

The EYE stack comprises the following Software and Machines:
[EYE-stack]

This is what the basic EAM (Euler Abstract Machine) does in a nutshell:

1. Select rule P => C
2. Prove P & NOT(C) (backward chaining) and if it fails backtrack to 1.
3. If P & NOT(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

• Design Issues of Tim Berners-Lee: The Semantic Web as a language of logic
• PhD thesis of Dörthe Arndt: Notation3 as the Unifying Logic for the Semantic Web
• Proposed built-ins of w3c N3: Vocabulary Definitions

See also

• EYE paper: Drawing Conclusions from Linked Data on the Web: The EYE Reasoner
• EYE tutorial: Semantic Web Reasoning With EYE
• EYE talk: EYE looking through N3 glasses