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:

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.

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: Notation3 Builtin Functions

Explainable Reasoning

Running the Semantic Web Databus and Proofbus from Tim Berners-Lee which is like a world wide welding machine transforming data into proofs:

EYE reasoning assumptions

• N3 rules can only have quickvars and they have rule scope
• Quickvars are interpreted universally except for forward rule conclusion-only variables which are interpreted existentially
• Blank nodes are interpreted existentially and have document scope

Examples and Test Cases

• bayesian networks: ccd, nbbn, swet
• control systems: acp, cs
• description logic: bmt, dt, edt, entail, gedcom, h2o, RDF plus OWL (source)
• ershovian compilation: preduction
• extensible imaging: lldm
• graph computation: graph, path-discovery
• logic programming: 4color, dp, diamond-property, gcc, hanoi, lee, n-queens, socrates, witch, zebra
• markovian networks: mmln
• mathematical reasoning: ackermann, eulers-identity, fibonacci, padovan, peano, peasant-multiplication, peasant-power, pi, polygon, tak
• neural networks: fcm, fgcm
• quantum computation: dqc
• universal machines: turing, usm
• workflow composers: gps, map, resto, restpath, twf

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
• N3 talk: Notation3 Logic: A Practical Introduction
• N3 editor: Notation3 Editor