Euler proof mechanism
Version 23.066 by Jos De Roo of AGFA
Problem
Generate a proof for a question about a given set of facts and rules.
For the authentication example
you can find who is authenticated
in authen.proof.rdf.
For the graph example
you can find a proof for the path question
in graph.proof.rdf.
For the lists example
you can see the proof of the list append question
in lists.proof.rdf.
Concept
The facts and rules are acquired from the Web and translated into a kind of logic program. The proof
engine only follows Euler paths (the concept Euler found several hundred years ago) so that
endless deductions are avoided. That means that no special attention have to be paid to recursions or
to graph merging.
Implementation
- The concept is implemented with the open source program Euler.java.
- Variables are identifiers starting with data:? prefix. That means that RDF subjects, predicates, and
objects can be unknowns at description time. The reason for variable predicates is to have support
for higher order logic and proof carrying mechanisms.
- A rule step ending with -not is meaning negation of that rule step.
- The extra-logical predicate http://www.agfa.com/w3c/euler#deref dereferences the subject URI and
unifies that value with the object. That means that scalable processing-by-delegation is possible.
- API
- public Euler() constructs a proof engine.
- public void assert(String uri) asserts all facts and rules in that proof engine.
- public String proof(String uri) proofs a conjunction with that proof engine.
History
- 23.066 axiom and lemma expressed in RDF syntax
- 23.065 proof expressed in RDF syntax
- 23.058 extra-logical predicate deref to dereference the subject URI
- 23.040 euler normal form syntax
- 22.040 predicates can be variables
- 22.006 reimplementation of euler circuit detection
- 22.003 change the syntax of negation to predicate-not
- 22.001 an implementation of forget when predicate is done
jos.deroo.jd@belgium.agfa.com