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:
- 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 premis of another sound argument.
Implementation
History
References
- http://www.w3.org/DesignIssues/Notation3.html
- http://www.w3.org/2000/10/swap/
- http://www.w3.org/2000/10/swap/Primer.html
- http://www.w3.org/2000/10/swap/Examples.html
- http://www.daml.org/2001/01/gedcom/gedcom-relations.xml
jos.deroo.jd@belgium.agfa.com