Using a First Order Logic Prover with OWL
We have been experimenting with the use of a First Order logic (FOL) reasoner in order to reason with OWL ontologies. This involves translating the OWL ontology into a collection of axioms suitable for a first order prover. Class references are translated to unary predicates, properties are translated to binary predicates and axioms are translated appropriately. For example, a subclass axiom:
Class( B partial A )
is translated to the axiom:
forall X. B(X) => A(X)
We can then use a FO prover (e.g. Vampire) to then, for example, check the consistency of the ontology.
A servlet that performs the translation from OWL to TPTP is available.
Using this approach, we are able to tackle a number of the OWL Tests, in particular those in the DL space. For each test type, the test is translated to a single collection of axioms, and the prover is asked to check the consistency of that collection.
- InconsistencyTest
- The ontology is converted to a collection of axioms. The prover is then asked to find a proof that the axioms are inconsistent.
- ConsistencyTest
- The ontology is converted to a collection of axioms and the prover is asked to demonstrate that the axioms are consistent (e.g. that it is unable to show that they are inconsistent). Due to the undecidability of FO reasoning, we cannot always guarantee that if the prover has not found a proof that one cannot be found. However, in many situations, the prover is able to demonstrate that it has employed a complete strategy and return a definitive result.
- PositiveEntailmentTest
- For positive entailment tests, we take the translation of the premises, add the negation of the translation of the conclusions and ask the prover to find an inconsistency. If one is found then the entailment holds.
- NegativeEntailmentTest
- These tests have not been attempted.
Note that this current strategy ignores annotations. This has no impact on the Consistency and Inconsistency tests. Our experiments regarding entailment tests, however, will need further investigation as annotations have an impact on entailment (in particular negative entailment).
Please also note that these are preliminary results of an experiment that will need further verification. These preliminary results are encouraging, however, and suggest that DL reasoners are feasible.
Test Results
We consider a number of possible different results:
- PASS
- The prover has returned a definitive result which is as expected.
- FAIL
- The prover returns a definitive result which is not as expected.
- UNKNOWN
- The prover has been unable to determine the satisfiability or unsatisfiability of the problem.
- UNKNOWN
- We have been unable to convert the problem to a suitable format for the prover, or an error occurred while running the prover thus the result is unknown.
- UNSUPPORTED
- The problem uses a datatype which is not supported by the reasoner (see below).
- TIMEOUT
- The reasoner ran out of time. The prover is currently allowed up to 300 seconds to find a proof.
Strictly speaking, any result other than PASS or UNSUPPORTED should be taken as a failure, however it is of use to distinguish between, for example a time out, an inability to find a proof, and a wrong answer.
Datatypes
The reasoner takes a very simple approach to datatypes, considering
two datatype values to be the same when they are lexically equivalent
(integers are canonicalised in a straightforward way). It also assumes
that the xsd:integer and xsd:string spaces are disjoint, and that
strings are different when they are not lexically equivalent. All
other data types are treated opaquely, e.g. if the values are
lexically identical they are considered to be equal. No other
assumptions are made (e.g. we do not assume inequality if the
lexical forms are not equal). Problems involving datatypes have been
attempted, but in the main will not succeed if the problem relies on
properties of the datatype. Problems which use unsupported datatypes
are labelled as UNSUPPORTED. The comment field
supplies some idea of the result that the reasoner produced (using the
assumptions above).
Details of Failures
As of 26/08/03, there is 1 test that FAIL:
Thing-001fails as the first order reasoner assumes that the domain is non-empty (i.e. there is an individual of typeowl:Thing). We are investigating possible solutions to this.
Six tests are classed as UNKNOWN. These include
those tests that include large cardinality constraints. The
translation rules result in the introduction of n+1
quantified variables for a cardinality constraint involving
n. Thus a constraint like cardinality(60000)
causes problems. Tests dl-903, dl-906,
dl-907, dl-909 and dl-910 fall
into this category. The reasoner runs out of memory (and then crashes)
on I5.21-002. For the four tests, the reasoner has
been unable to determine the (un)satisfiability of the problem.
Fourteen tests use UNSUPPORTED datatypes.
Tests Attempted
For each test we show the kind of test, the time taken in seconds (reported by Vampire) and the result. Comments supply extra information and for UNSUPPORTED tests the datatypes found in the test are reported.
| Type | Level | Test | Time (s) | Result | Comment | Datatypes |
|---|---|---|---|---|---|---|
| Consistency | DL | description-logic--005 | 0 | PASS | ||
| Consistency | DL | description-logic--006 | 0 | PASS | ||
| Consistency | DL | description-logic--009 | 0 | PASS | ||
| Consistency | DL | description-logic--016 | 0 | PASS | ||
| Consistency | DL | description-logic--018 | 0 | PASS | ||
| Consistency | DL | description-logic--020 | 1.6 | PASS | ||
| Consistency | DL | description-logic--021 | 174.5 | PASS | ||
| Consistency | DL | description-logic--024 | 0 | PASS | ||
| Consistency | DL | description-logic--025 | 0 | PASS | ||
| Consistency | DL | description-logic--028 | 0 | PASS | ||
| Consistency | DL | description-logic--031 | 0 | PASS | ||
| Consistency | DL | description-logic--034 | 0 | PASS | ||
| Consistency | DL | description-logic--501 | 300.1 | TIMEOUT | ||
| Consistency | DL | description-logic--503 | 0 | PASS | ||
| Consistency | Lite | description-logic--605 | 0 | PASS | ||
| Consistency | Lite | description-logic--606 | 0 | PASS | ||
| Consistency | Lite | description-logic--609 | 0 | PASS | ||
| Consistency | Lite | description-logic--616 | 0 | PASS | ||
| Consistency | Lite | description-logic--624 | 0 | PASS | ||
| Consistency | Lite | description-logic--625 | 0 | PASS | ||
| Consistency | Lite | description-logic--628 | 1.3 | UNKNOWN | No proof found | |
| Consistency | Lite | description-logic--631 | 1.3 | UNKNOWN | No proof found | |
| Consistency | Lite | description-logic--634 | 0 | PASS | ||
| Consistency | DL | description-logic--905 | 300.1 | TIMEOUT | ||
| Consistency | DL | description-logic--906 | UNKNOWN | Large cardinality constraint | ||
| Consistency | DL | description-logic--907 | UNKNOWN | Large cardinality constraint | ||
| Consistency | DL | description-logic--908 | 3.4 | PASS | ||
| Consistency | DL | disjointWith--003 | 0 | PASS | ||
| Consistency | DL | disjointWith--005 | 0 | PASS | ||
| Consistency | DL | disjointWith--007 | 0 | PASS | ||
| Consistency | DL | disjointWith--009 | 0 | PASS | ||
| Consistency | DL | equivalentClass--009 | 0 | PASS | ||
| Consistency | Lite | I5.2--001 | 0 | PASS | ||
| Consistency | Lite | I5.2--003 | 0 | PASS | ||
| Consistency | DL | I5.2--005 | 0 | PASS | ||
| Consistency | Lite | I5.2--010 | 0 | PASS | ||
| Consistency | Lite | I5.2--011 | 0 | PASS | ||
| Consistency | Lite | I5.3--006 | 0 | PASS | ||
| Consistency | Lite | I5.3--008 | 0 | PASS | ||
| Consistency | Lite | I5.3--011 | 0 | PASS | ||
| Consistency | DL | I5.8--002 | 12.6 | UNSUPPORTED | unknown | xsd:byte |
| Consistency | DL | I5.8--012 | 2.1 | UNSUPPORTED | unknown | xsd:byte, xsd:unsignedInt |
| Consistency | DL | miscellaneous--001 | 300.1 | UNSUPPORTED | timeout | xsd:positiveInteger |
| Consistency | DL | miscellaneous--002 | 300.1 | UNSUPPORTED | timeout | xsd:positiveInteger |
| Consistency | DL | miscellaneous--102 | 0 | PASS | ||
| Consistency | DL | miscellaneous--103 | 0 | PASS | ||
| Consistency | Lite | miscellaneous--201 | 0 | PASS | ||
| Consistency | Lite | miscellaneous--202 | 0 | PASS | ||
| Consistency | Lite | miscellaneous--205 | 0 | PASS | ||
| Consistency | Lite | miscellaneous--303 | 0 | PASS | ||
| Consistency | Lite | Restriction--004 | 0 | PASS | ||
| Consistency | Lite | Thing--001 | 0 | FAIL | Proof found! | |
| Inconsistency | DL | description-logic--001 | 0 | PASS | ||
| Inconsistency | DL | description-logic--002 | 0 | PASS | ||
| Inconsistency | DL | description-logic--003 | 0 | PASS | ||
| Inconsistency | DL | description-logic--004 | 0 | PASS | ||
| Inconsistency | DL | description-logic--007 | 0 | PASS | ||
| Inconsistency | DL | description-logic--008 | 0 | PASS | ||
| Inconsistency | DL | description-logic--010 | 0 | PASS | ||
| Inconsistency | DL | description-logic--011 | 0 | PASS | ||
| Inconsistency | DL | description-logic--012 | 0 | PASS | ||
| Inconsistency | DL | description-logic--013 | 0 | PASS | ||
| Inconsistency | DL | description-logic--014 | 0 | PASS | ||
| Inconsistency | DL | description-logic--015 | 0 | PASS | ||
| Inconsistency | DL | description-logic--017 | 0 | PASS | ||
| Inconsistency | DL | description-logic--019 | 0.1 | PASS | ||
| Inconsistency | DL | description-logic--022 | 1.3 | PASS | ||
| Inconsistency | DL | description-logic--023 | 0 | PASS | ||
| Inconsistency | DL | description-logic--026 | 0 | PASS | ||
| Inconsistency | DL | description-logic--027 | 0 | PASS | ||
| Inconsistency | DL | description-logic--029 | 0 | PASS | ||
| Inconsistency | DL | description-logic--030 | 0 | PASS | ||
| Inconsistency | DL | description-logic--032 | 0 | PASS | ||
| Inconsistency | DL | description-logic--033 | 0 | PASS | ||
| Inconsistency | DL | description-logic--035 | 0 | PASS | ||
| Inconsistency | DL | description-logic--101 | 0 | PASS | ||
| Inconsistency | DL | description-logic--102 | 0 | PASS | ||
| Inconsistency | DL | description-logic--103 | 0 | PASS | ||
| Inconsistency | DL | description-logic--104 | 0 | PASS | ||
| Inconsistency | DL | description-logic--105 | 0 | PASS | ||
| Inconsistency | DL | description-logic--106 | 0 | PASS | ||
| Inconsistency | DL | description-logic--107 | 0 | PASS | ||
| Inconsistency | DL | description-logic--108 | 0 | PASS | ||
| Inconsistency | DL | description-logic--109 | 0 | PASS | ||
| Inconsistency | DL | description-logic--110 | 0 | PASS | ||
| Inconsistency | DL | description-logic--111 | 0 | PASS | ||
| Inconsistency | DL | description-logic--502 | 300.1 | TIMEOUT | ||
| Inconsistency | DL | description-logic--504 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--601 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--602 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--603 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--604 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--608 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--610 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--611 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--612 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--613 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--614 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--615 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--617 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--623 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--626 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--627 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--629 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--630 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--632 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--633 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--641 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--642 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--643 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--644 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--646 | 0 | PASS | ||
| Inconsistency | Lite | description-logic--650 | 0 | PASS | ||
| Inconsistency | DL | description-logic--909 | UNKNOWN | Large cardinality constraint | ||
| Inconsistency | DL | description-logic--910 | UNKNOWN | Large cardinality constraint | ||
| Inconsistency | DL | I4.5--002 | 0 | PASS | ||
| Inconsistency | DL | I5.8--001 | 13 | UNSUPPORTED | unknown | xsd:byte |
| Inconsistency | DL | I5.8--003 | 2.1 | UNSUPPORTED | unknown | xsd:byte, xsd:unsignedInt |
| Inconsistency | Lite | miscellaneous--203 | 0 | UNSUPPORTED | fail | rdf:XMLLiteral |
| Inconsistency | Lite | miscellaneous--204 | 0 | UNSUPPORTED | fail | rdf:XMLLiteral |
| Inconsistency | Lite | Nothing--001 | 0 | PASS | ||
| Inconsistency | Lite | Restriction--001 | 0 | PASS | ||
| Positive Entailment | Lite | allValuesFrom--001 | 0 | PASS | ||
| Positive Entailment | Lite | cardinality--001 | 0 | PASS | ||
| Positive Entailment | Lite | cardinality--002 | 0 | PASS | ||
| Positive Entailment | DL | cardinality--003 | 0 | PASS | ||
| Positive Entailment | DL | cardinality--004 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--201 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--202 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--203 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--204 | 0.1 | PASS | ||
| Positive Entailment | DL | description-logic--205 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--206 | 0.4 | PASS | ||
| Positive Entailment | DL | description-logic--207 | 0 | PASS | ||
| Positive Entailment | DL | description-logic--208 | 189.7 | UNKNOWN | No proof found | |
| Positive Entailment | Lite | description-logic--661 | 0.1 | PASS | ||
| Positive Entailment | Lite | description-logic--662 | 0.1 | PASS | ||
| Positive Entailment | Lite | description-logic--663 | 0.1 | PASS | ||
| Positive Entailment | Lite | description-logic--664 | 0.2 | PASS | ||
| Positive Entailment | Lite | description-logic--665 | 0 | PASS | ||
| Positive Entailment | Lite | description-logic--666 | 1 | PASS | ||
| Positive Entailment | Lite | description-logic--667 | 0 | PASS | ||
| Positive Entailment | Lite | description-logic--668 | 287.4 | UNKNOWN | No proof found | |
| Positive Entailment | DL | description-logic--901 | 1 | PASS | ||
| Positive Entailment | DL | description-logic--903 | UNKNOWN | Large cardinality constraint | ||
| Positive Entailment | DL | disjointWith--001 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentClass--001 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentClass--002 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentClass--003 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentClass--004 | 0 | PASS | ||
| Positive Entailment | DL | equivalentClass--006 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentProperty--001 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentProperty--002 | 0 | PASS | ||
| Positive Entailment | Lite | equivalentProperty--003 | 0 | PASS | ||
| Positive Entailment | DL | equivalentProperty--004 | 0 | PASS | ||
| Positive Entailment | DL | I4.5--001 | 0 | PASS | ||
| Positive Entailment | Lite | I5.2--002 | 0 | PASS | ||
| Positive Entailment | DL | I5.2--004 | 0 | PASS | ||
| Positive Entailment | DL | I5.2--006 | 0 | PASS | ||
| Positive Entailment | DL | I5.21--002 | UNKNOWN | No Results | ||
| Positive Entailment | Lite | I5.24--003 | 0 | PASS | ||
| Positive Entailment | Lite | I5.24--004 | 0 | PASS | ||
| Positive Entailment | DL | I5.8--004 | 2 | UNSUPPORTED | unknown | xsd:byte, xsd:unsignedInt |
| Positive Entailment | Lite | I5.8--006 | 0 | UNSUPPORTED | fail | xsd:short, xsd:byte |
| Positive Entailment | Lite | I5.8--008 | 0 | UNSUPPORTED | fail | xsd:unsignedShort, xsd:short, xsd:unsignedInt |
| Positive Entailment | Lite | I5.8--009 | 0 | UNSUPPORTED | fail | xsd:nonPositiveInteger, xsd:nonNegativeInteger, xsd:short |
| Positive Entailment | Lite | I5.8--010 | 0 | UNSUPPORTED | fail | xsd:nonNegativeInteger, xsd:nonPositiveInteger, xsd:int |
| Positive Entailment | DL | oneOf--004 | 0 | UNSUPPORTED | fail | xsd:short |
| Positive Entailment | DL | unionOf--003 | 0 | PASS | ||
| Positive Entailment | DL | unionOf--004 | 0 | PASS |
Result Summary
| Type | Attempted | PASS | FAIL | UNKNOWN | UNKNOWN | UNSUPPORTED | TIMEOUT | % PASS | % PASS (all supported tests) |
|---|---|---|---|---|---|---|---|---|---|
| Inconsistent | 70 | 63 | 2 | 4 | 1 | 90 | 95 | ||
| Consistent | 52 | 41 | 1 | 2 | 2 | 4 | 2 | 78 | 85 |
| Positive | 48 | 38 | 2 | 2 | 6 | 79 | 90 | ||
| Total | 170 | 142 | 1 | 4 | 6 | 14 | 3 | 83 | 91 |
OWL-Lite Test results
| Type | Attempted | PASS | FAIL | UNKNOWN | UNKNOWN | UNSUPPORTED | TIMEOUT | % PASS | % PASS (all supported tests) |
|---|---|---|---|---|---|---|---|---|---|
| Inconsistent | 29 | 27 | 2 | 93 | 100 | ||||
| Consistent | 22 | 19 | 1 | 2 | 86 | 86 | |||
| Positive | 25 | 20 | 1 | 4 | 80 | 95 | |||
| Total | 76 | 66 | 1 | 3 | 6 | 86 | 94 |
Sean Bechhofer, University of Manchester, 03/01/04
