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 .
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 .
The detailed design of EYE comprises:
1/ N3  parser specified as Prolog DCG (Definite Clause Grammar)
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/ 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 .
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  and their results  support the development of EYE.
EYE is a reasoning engine supporting the RGB Semantic Web layers 
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
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
o Implicit Quantification in N3
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 Blueproof without @ keywords
o Blueproof without bindings