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:
The EYE test cases  and their results  support the EYE development.
EYE is a reasoning engine supporting the RGB Semantic Web layers 
i.e. RDF entities + unifying logic + explainable reasoning.
RDF entities 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
For EYE the interpretation of L0 => L1 is the clause ~L0 | L1.
The scope of implicit universals is the clause ~L0 | L1.
The scope of implicit existentials is the positive clause literal Li.
Blank node labels are only valid within the current graph 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
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 .