EYE note

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 reasoner enhanced with Euler path detection. Semibackward reasoning is backward reasoning for EYE components i.e. rules using <= in N3 and forward reasoning for rules using => in N3. 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. 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". 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 [Logic]. The detailed design of EYE comprises: 1/ N3 parser specified as Prolog rules 2/ N3Logic to N3P (N3 P-code) compiler 3/ EAM (Euler Abstract Machine) with Euler path detection to avoid loops 4/ proof construction using the vocabulary for proofs 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) 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/ or 1/ 5/ If brake or tactic linear-select stop, else start again at 1/ This is how the current EYE integration is worked out: EYE 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 built-ins o RIF Datatypes and Built-Ins o Prolog built-ins o Implicit Quantification in N3 An EYE 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. The scope of implicit universals is the clause. The scope of implicit existentials is the clause literal. 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 output without @ keywords o Proof output without bindings P.S. In the future, reasoners could have a large impact on software. A few decades ago, software took over many jobs from hardware: calculations that used to be hard-wired became soft-wired as lines of code. Although some highly optimized calculations still happen in hardware, most are now performed with special-purpose software on generic-purpose hardware. Similarly, reasoners will start rewiring software for specific situations. EYE already does this when performing rule-based Web service composition. In the end, this opens the door to automatically customized software processes. What software once did for hardware, reasoning might one day do for software [EYE paper].