Current development of EYE open source reasoning engine is going on at https://github.com/josd/eye.

Euler Proof Mechanism

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 and LICENSE.
The software is maintained at EulerSharp.
Things are described in N3 thanks to Tim Berners-Lee and Dan Connolly.

EYE

Problem

Given a set of facts and rules, ask a question and get a proof for it.

for authentication example ask who is authenticated and get authen.proof.n3
for graph example ask path question and get graph.proof.n3
for gedcom-relations.n3 and gedcom-facts.n3 ask gedcom-query.n3 and get gedcom-proof.n3
for danc.n3 ask danc-query.n3 and get danc-result.n3
for ziv.n3 ask ziv-query.n3 and get ziv-result.n3
for danb.n3 ask danb-query.n3 and get danb-result.n3
for deb.n3 ask debC.n3 and get debE.n3
for animal.n3 ask animal-simple.n3 and get animal-result.n3
for subprop.n3 ask subprop-query.n3 and get subprop-result.n3
for subclass.n3 ask subclass-query.n3 and get subclass-result.n3
for test.n3 ask test-test.n3 and get test-result.n3
ask builtins.n3 and get builtins-result.n3
for easterP.n3 ask easterC.n3 and get easterE.n3
for dtP.n3 ask dtC.n3 and get dtE.n3
for rdfs-rules.n3 and rdfs-facts.n3 ask rdfs-query.n3 and get rdfs-result.n3
for owl-rules.n3 and owl-facts.n3 ask owl-query.n3 and get owl-result.n3
ask etc1.n3 and get etc1-proof.n3
ask etc2.n3 and get etc2-proof.n3
ask etc3.n3 and get etc3-proof.n3
ask etc4.n3 and get etc4-proof.n3

Concept

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.

The so called proof thing is a SOUND ARGUMENT:

An ARGUMENT is a pair of things:
- a set of sentences, the PREMISES;
- a sentence, the CONCLUSION.
An argument is VALID if and only if it is necessary that if all its premises are true, its conclusion is true.
An argument is SOUND if and only if it is valid and all its premises are true.
A sound argument can be the premise of another sound argument.

Jos De Roo