Euler proof mechanism

$Id: index.html,v 1.402 2004/01/25 19:38:43 amdus Exp $ Version R3680 by Jos De Roo of AGFA.
See Euler FAQ at EulerSharp and see also W3C Cwm.

Testing (*) RDF test cases obtaining RDF test results and testing OWL test cases obtaining OWL test results
using rule sets such as rdfs-rules, xsd-rules, owl-rules, log-rules, ...

(*) Test cases have a THIS part and a THAT part such that assuming the THIS part implies the THAT part.
Test cases have explicit assumptions because assumptions should be checked.
Test cases make issues observable (both issues w.r.t. requirements and designissues).
Test cases lead to test results which are one of passing, failing, undecided or no-data.
Test cases can be in the following state: proposed, approved, extra-credit or obsoleted.

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 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
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
...
or just ask etc3.n3 and get etc3-proof.n3
or just ask etc4.n3 and get etc4-proof.n3
or just ask etc5.n3 and get etc5-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 premis of another sound argument.

Implementation

Things are described in N3 thanks to Tim Berners-Lee and Dan Connolly.
The concept is implemented with the open source programs Euler.java and Parser.java as well as with EulerSharp.
API
- Euler class
- Parser class
Usage
- Unzip euler.zip in [path] and place [path] in your classpath (for RDF/XML to N3 triple generation also Jena2 is needed).
- java [-Dhttp_proxy=%http_proxy%] Euler [--think] [--nope] [--step count] [--debug] [--trace] axiom ... lemma
Issues
- duplicate rule elimination
- clause/premis reordering
- CWM builtins

History

R3680 corrected _:X a rdfs:Literal derivation
R3666 corrected trigonometric builtins + no need for occurs check + use @has again when a fact has to be explicitly given
R3659 using s [= p] o instead of s has p o + corrected comprehension principle + corrected nonentailments
R3653 using log:racine in rule premis
R3644 XML and XSD clashes are inconsistencies
R3636 corrections wrt proof check
R3634 correct/simplify toString for :a :b {:c :d :e}.
R3632 added log:notImplies again to run negative entailment and consistency tests
R3631 try kind of proof checking in etc4-proof
R3629 parser reports line numbers in error messages + improved clash detection
R3626 builtins math:atan2 math:cos math:cosh math:degrees math:sin math:sinh math:tan math:tanh
R3624 shorter proofs using iw:Variable
R3622 added method to detect XML clash and datatype clash
R3618 correction for getting URI's with hash
R3612 shorter prepare time
R3604 only ground terms in proof
R3601 fixing owl:equivalentClass reflexivity problem
R3588 be explicit about which rule sets in etc
R3587 fixing comprehension problem
R3584 not trying to extend Euler paths
R3582 corrected bug in eval for {triples} => {{triples} log:inconsistentWith theory}.
R3573 not running negative entailment tests and consistency tests
R3567 added resultsOntology:IncompleteRun
R3564 :X^^:Y is not necessarily a :Y
R3561 some corrections to work with Jena-2.0
R3558 start using testresult ontology
R3550 beginning of Euler path extensions
R3548 some improvements for owl:sameAs
R3540 bug correction in parsing of lists with typed literals
R3539 builtin string:contains and string:containsIgnoringCase + use Jena-2.0.0-beta1 to parse RDF/XML files (see FAQ)
R3532 testing OWL Manifest and obtaining testresults
R3520 testing OWL Manifest
R3514 testing with mono-0.25
R3507 simplified eval + corrected log:includes output
R3489 got back to simple rule indicators
R3484 primitive goal reordering + partial OWL comprehension conditions
R3479 3rd major attempt (in 2 years) to tackle variable verbs in rule conclusions
R3474 2 fixes in fromWeb(uri) thanks to Peter Kenens and Jeffrey Hau
R3472 builtin str:equalIgnoringCase and str:notEqualIgnoringCase
R3470 corrected nasty bug in the relabeling of bnodes across multiple documents, thanks to Jeffrey Hau
R3469 running OWL Lite and DL level tests + OWLforOWLTest
R3466 owl-rules corrections/simplifications thanks to PeterPS
R3454 command line switch --nope to have no proof explanation
R3448 follow paths such that test entails test-test
R3444 added owl:AllDisjoint
R3442 :jenny :age 15. now being proved given :jenny :age [is math:sum of (10 5)].
R3440 update so that dtP entails dtC
R3435 fixed unify in calling occurs check
R3433 current-file rdfs:fyi rule-id (instead of just rule-id)
R3431 use [ iw:Variable "?X"] = value to talk about the bindings in a proof argument
R3427 use reason:unknownBecause when no proof found + rewrite :a.:b paths
R3426 start to (mis?)use reason:because in proof generations
R3425 added rdf:TriviallyTrue
R3421 OWL Full test result etc5-proof.n3
R3417 added owl-rules#owl8s7 thanks to Jeremy
R3415 took out some wrong entailments
R3413 support math:absoluteValue, math:rounded, math:integerQuotient (now used in easterP.n3)
R3411 support unquoted numerals in proof output
R3406 correction in unify
R3389 more dot fun in supporting unquoted N3 numerals such as 2.0 and 2.0e3
R3384 use forward paths in etc5
R3376 implement forward paths and test easterC.n3 given easterP.n3
R3368 trying negation stuff at end of owl-rules
R3356 giving up on all the negation stuff such as log:Falsehood, owl:complementOf, rdft:NegativeEntailmentTest, owlt:NegativeEntailmentTest
R3353 Skolem function ?x1^^?x2...^^_:abc to replace existentials in conclusions + correction in eval
R3349 explanation of the substitutions in the proof as {... ?s = :a. ?p = :b. ?o = :c. ?s ?p ?o} log:implies {:a :b :c}.
R3338 builtin log:definitiveDocument and log:definitiveService using log-rules
R3333 change to owl:equivalentClass and owl:equivalentProperty + prove Jeremy's Ugly Test
R3325 use log:conjunction and log:semantics in etc5
R3320 now assuming that a plain literal is an xsd:string + builtin that a typed literal is of that type + etc5 running 3 times faster
R3314 more owl testcases + test owl:AllDifferent and owl:distinctMembers + owl:Property
R3311 going back to owl:Class and owl:sameClassAs
R3306 talk and test