Euler proof mechanism

Version 27.035 -- last modified 2001/08/05 -- 22:21:00 GMT -- by Jos De Roo of AGFA

Problem

Generate a proof for a question about a given set of facts and rules.

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:

Implementation

History

References

  1. http://www.w3.org/DesignIssues/Notation3.html
  2. http://www.w3.org/2000/10/swap/
  3. http://www.w3.org/2000/10/swap/Primer.html
  4. http://www.w3.org/2000/10/swap/Examples.html
  5. http://www.daml.org/2001/01/gedcom/gedcom-relations.xml
jos.deroo.jd@belgium.agfa.com