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
i.e. rules using <= in N3 and backward-forward-backward reasoning
for rules using => in N3. 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/ 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/
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 built-ins
o RIF Datatypes and Built-Ins
o Prolog built-ins
o Implicit Quantification in N3
A N3 resource contains implications of the form Li => Lj
and a conjunction of the remaining triples Lz.
The interpretation of Li => Lj is the clause ~Li | Lj
and the interpretation of Lz is the clause Lz.
Li, Lj and Lz 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
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 .