EYE stands for "Euler Yet another proof Engine" and it is a further development of Euler which is an inference engine supporting logic based proofs. EYE is a semibackward reasoning engine enhanced with Euler path detection. The Euler path detection is 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 [1]. EYE sees the rule P => C as P & NOT(C) => C so it follows so called PNC steps (PNC stands for "Premis and Not Conclusion"). Semibackward reasoning is pure backward reasoning for backward rules (rules using <= in N3) and backward-forward-backward reasoning for forward rules (rules using => in N3). The backward-forward-backward reasoning is realized via an underlying Prolog backward chaining, a forward meta-level reasoning and a backward proof construction. The reasoning that EYE is performing is grounded in FOL (First Order Logic). Keeping a language less powerful than FOL is quite reasonable within an application, but not for the Web [2]. The detailed design of EYE comprises: 1/ N3 [3] parser specified as Prolog DCG (Definite Clause Grammar) 2/ N3Logic [4] to N3P (Notation 3 P-code) compiler 3/ EAM (Euler Abstract Machine) with Euler path detection to avoid loops and with postponed brake mechanism to run at much increased speed 4/ proof construction using the vocabulary for proofs [5] 5/ builtins 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) 3/ If P & NOT(C) assert C (forward chaining) 4/ If C = answer(A) and tactic single-answer stop, else backtrack to 2/ or 1/ 5/ If brake or tactic linear-logic stop, else start again at 1/ In the current design of EYE things are layered and cascaded as follows: High performance is crucial and that is the main reason why EYE is depending on flexible indexing of Prolog clauses during runtime [6]. Indexing Prolog clauses on demand during program execution, also called JITI (Just In Time Indexing) or DDI (Demand Driven Indexing) can really make a substantial difference and is in that respect very similar to indexing used for relational databases. Even a small percentage of badly indexed calls can end up dominating runtime. The EYE test cases [7] and their results [8] support the development of EYE. Designissues ------------ EYE is a reasoning engine supporting the RGB Semantic Web layers [9] i.e. Linked Data plus EULER = Unifying Logic + Explainable Reasoning. Linked Data goes back to the very essence of the Web and information itself, by representing each piece of data as a link between two things. o Turtle without @ keywords o Notation 3 graph literals Unifying Logic designates a logic framework that can be shared across different agents on the Web. Some basic blocks are best exposed through built-ins, special predicates that are not necessarily implemented in N3. In order for agents to communicate with each other, they have to agree on a predefined set of built-ins with a rigorously specified meaning - if not, results and corresponding proofs cannot be trusted. o Cwm Built-in functions o Logic Framework Extension builtins o RIF Datatypes and Built-Ins o Prolog builtins Explainable reasoning indicates the possibility of agents to produce and exchange proofs. Any conclusion reached by a reasoner must be independently verifiable to enable real-world applications. o Proof construction using the proof vocabulary o Proof without @ keywords and without bindings References ---------- [1] http://mathworld.wolfram.com/KoenigsbergBridgeProblem.html [2] http://www.w3.org/DesignIssues/Logic [3] http://www.w3.org/TeamSubmission/n3/ [4] http://www.w3.org/DesignIssues/N3Logic [5] http://www.w3.org/2000/10/swap/reason [6] http://user.it.uu.se/~kostis/Papers/iclp07.pdf [7] http://eulersharp.sourceforge.net/2006/02swap/etc.sh [8] http://eulersharp.sourceforge.net/2006/02swap/etc.n3 [9] http://www.w3.org/DesignIssues/diagrams/sweb-stack/2006a