EYE readme

EYE is a reasoning engine supporting the RGB Semantic Web layers [1].
It performs semibackward reasoning and it supports Euler paths.

Semibackward reasoning is backward reasoning for EYE components i.e.
rules using <= in N3 and forward reasoning for rules using => in N3.

Euler paths are roughly "don't step in your own steps" and in that
respect there is a similarity with what Leonhard Euler discovered
in 1736 for the Königsberg Bridge Problem [2]. EYE sees the rule
P => C as P & NOT(C) => C.

Via N3 [3] EYE is interoperable with Cwm [4].

ETC [5] is used to verify EYE releases [6].

EYE can be installed manually on Linux, Windows and MacOSX [7].
EYE is also available in a Docker container for command line use [8]
and in a Docker container for HTTP client use [9].

The main building blocks of EYE are depicted in [10].

The detailed design of EYE comprises:
 1/ N3 [3] parser specified as Prolog rules
 2/ N3Logic [11] to N3P (N3 P-code) compiler
 3/ EAM (Euler Abstract Machine) supporting Euler paths
 4/ proof construction using the vocabulary for proofs [12]
 5/ built-ins and support predicates for the above functionalities

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 single-answer stop, else backtrack to 2/
 5/ If brake or tactic linear-select stop, else start again at 1/


Design issues
-------------

Implicit Quantification in N3 [13]
  A N3 resource contains implications of the form Li => Lj or
  Lj <= Li and a conjunction of the remaining statements L0.
  Li => Lj, Lj <= Li and L0 are called clauses.
  Li, Lj and L0 are called clause literals.
  In ETC [5] the scope of implicit universals is the clause and
  the scope of implicit existentials is the clause literal.

Proof output without bindings [14]
  In ETC [5] the variable substitutions naturally follow from the proof.


See also
--------

EYE paper [15]
  Drawing Conclusions from Linked Data on the Web: The EYE Reasoner

EYE tutorial [16]
  Semantic Web Reasoning With EYE

EYE talk [17]
  EYE looking through N3 glasses

EYE logo [18]


References
----------

 [1] http://www.w3.org/DesignIssues/diagrams/sweb-stack/2006a
 [2] http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html
 [3] http://www.w3.org/TeamSubmission/n3/
 [4] http://www.w3.org/2000/10/swap/doc/cwm
 [5] https://github.com/josd/etc
 [6] https://github.com/josd/eye/blob/master/RELEASE
 [7] https://github.com/josd/eye/blob/master/INSTALL
 [8] https://registry.hub.docker.com/u/bdevloed/eye/
 [9] https://registry.hub.docker.com/u/bdevloed/eyeserver/
[10] http://josd.github.io/images/eye-reasoning-engine.png
[11] http://www.w3.org/DesignIssues/N3Logic
[12] http://www.w3.org/2000/10/swap/reason.n3
[13] https://lists.w3.org/Archives/Public/public-cwm-talk/2015JanMar/0000
[14] http://josd.github.io/etc/witch/witch-proof.n3
[15] http://online.qmags.com/ISW0515?cid=3244717&eid=19361&pg=25#pg25&mode2
[16] http://n3.restdesc.org/
[17] http://www.agfa.com/w3c/Talks/2012/04swig/
[18] http://josd.github.io/images/eye.png