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 issue: 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. Design issue: Proof output without bindings [14] In ETC [5] the variable substitutions naturally follow from the proof. [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