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.