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.

The ontology is converted to a collection of axioms. The prover is then asked to find a proof that the axioms are inconsistent.
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.
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.
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:

The prover has returned a definitive result which is as expected.
The prover returns a definitive result which is not as expected.
The prover has been unable to determine the satisfiability or unsatisfiability of the problem.
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.
The problem uses a datatype which is not supported by the reasoner (see below).
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.


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:

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.

TypeLevelTestTime (s)ResultCommentDatatypes
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 UNKNOWNNo proof found
Consistency Lite description-logic--631 1.3 UNKNOWNNo proof found
Consistency Lite description-logic--634 0 PASS
Consistency DL description-logic--905 300.1 TIMEOUT
Consistency DL description-logic--906 UNKNOWNLarge cardinality constraint
Consistency DL description-logic--907 UNKNOWNLarge 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 UNSUPPORTEDunknownxsd:byte
Consistency DL I5.8--012 2.1 UNSUPPORTEDunknownxsd:byte, xsd:unsignedInt
Consistency DL miscellaneous--001 300.1 UNSUPPORTEDtimeoutxsd:positiveInteger
Consistency DL miscellaneous--002 300.1 UNSUPPORTEDtimeoutxsd: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 FAILProof 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 UNKNOWNLarge cardinality constraint
Inconsistency DL description-logic--910 UNKNOWNLarge cardinality constraint
Inconsistency DL I4.5--002 0 PASS
Inconsistency DL I5.8--001 13 UNSUPPORTEDunknownxsd:byte
Inconsistency DL I5.8--003 2.1 UNSUPPORTEDunknownxsd:byte, xsd:unsignedInt
Inconsistency Lite miscellaneous--203 0 UNSUPPORTEDfailrdf:XMLLiteral
Inconsistency Lite miscellaneous--204 0 UNSUPPORTEDfailrdf: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 UNKNOWNNo 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 UNKNOWNNo proof found
Positive Entailment DL description-logic--901 1 PASS
Positive Entailment DL description-logic--903 UNKNOWNLarge 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 UNKNOWNNo Results
Positive Entailment Lite I5.24--003 0 PASS
Positive Entailment Lite I5.24--004 0 PASS
Positive Entailment DL I5.8--004 2 UNSUPPORTEDunknownxsd:byte, xsd:unsignedInt
Positive Entailment Lite I5.8--006 0 UNSUPPORTEDfailxsd:short, xsd:byte
Positive Entailment Lite I5.8--008 0 UNSUPPORTEDfailxsd:unsignedShort, xsd:short, xsd:unsignedInt
Positive Entailment Lite I5.8--009 0 UNSUPPORTEDfailxsd:nonPositiveInteger, xsd:nonNegativeInteger, xsd:short
Positive Entailment Lite I5.8--010 0 UNSUPPORTEDfailxsd:nonNegativeInteger, xsd:nonPositiveInteger, xsd:int
Positive Entailment DL oneOf--004 0 UNSUPPORTEDfailxsd:short
Positive Entailment DL unionOf--003 0 PASS
Positive Entailment DL unionOf--004 0 PASS

Result Summary

Inconsistent 70632419095
Consistent 5241122427885
Positive 48382267990
Total 1701421461438391

OWL-Lite Test results

Inconsistent 2927293100
Consistent 2219128686
Positive 2520148095
Total 76661368694

Sean Bechhofer, University of Manchester, 03/01/04