Semantic Web | RDF | OWL

$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. |

- 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

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.

- 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
- 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

- 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