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-select stop, else start again at 1/

In the current design of EYE things are integrated 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.


EYE is a reasoning engine supporting the RGB Semantic Web layers [9]
i.e. RDF endpoints + unifying logic + explainable reasoning.

RDF endpoints go 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


 [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