EYE is an inference engine supporting logic based proofs. It is a backward-forward-backward chaining reasoner enhanced with Euler path detection.
The backward-forward-backward chaining is realized via an underlying Prolog backward chaining, a forward meta-level reasoning and a backward proof construction.