Euler proof mechanism (original) (raw)

Euler is an inference engine supporting logic based proofs.
It is a backward-chaining reasoner enhanced with Euler path detection.
It has implementations in Java, C#, Python, Javascript and Prolog.
Via N3 it is interoperable with W3C Cwm.

See DONE,README,INSTALL,BUILD,GUIDE,FAQ andLICENSE.
The software is maintained at EulerSharp.
Things are described in N3 thanks toTim Berners-Lee andDan Connolly.

         EYE
        

The axioms are acquired from the Web and translated into a kind of logic program. The proof engine uses the resolution inference mechanism and only follows Euler paths (the concept Euler found several hundred years ago) so that endless deductions are avoided. That means that no special attention has to be paid to recursions or to graph merging.