# 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 reasoning engine
supporting the RGB Semantic Web layers.
EYE performs semibackward reasoning and it supports Euler paths.
Semibackward reasoning is backward reasoning for EYE components i.e.
rules using <= in N3 and forward reasoning for rules using => in N3.
Euler paths are 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.
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) supporting Euler paths
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) and if it fails backtrack to 1/
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/
5/ If brake or tactic linear-select stop, else start again at 1/
This is the EYE proof engine:
**Design issue:** Implicit Quantification in N3
A N3 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.
**Design issue:** Proof output without bindings
The variable substitutions naturally follow from the proof.