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.

ulr (euler who lost 2 e'yes)

  • queries use an upwards double arrow =^
  • backward rules use a leftwards double arrow <=
  • forward rules use a rightwards double arrow =>
  •             eye                      observership
                 u                        /        \
                =^                       /          \
           l <= eye => r            origin ------- evolution


  • only _:x blank nodes in triples and quads
  • only ?x quickvars in rules and queries
  • quantified var:x variables in proofs
  • 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