The Web Ontology Language OWL 2 DL is the language used to build ontologies for a wide range of domains including the life sciences, the financial industry and the domain of energy simulations. Many of these domain ontologies are built beneath upper ontologies (such as DOLCE or BFO), which themselves are written in more expressive logics than OWL 2 DL, in particular first-order logic (although they may provide truncated versions in OWL). In this paper we present FOWL, a tool that enables the translation of OWL ontologies into FOL, and thereby the integration of OWL domain ontologies with ifrst-order logic ontologies. One use case for this tool is the ability to validate OWL domain ontologies against their upper-level ontology. FOWL also allows reasoning over the translation using the VAMPIRE reasoner.
that cannot be expressed in OWL. However, without tool support it is not possible to integrate both into a whole that can be reasoned with.
In this paper we present FOWL, a tool that enables the automatic translation of OWL ontologies into FOL (in particular, the TPTP syntax for first-order theories). We start by describing our approach to the translation on a theoretical level. Afterwards we take a look at how FOWL works and can be used in practice. We also evaluate the performance of FOWL and discuss related work as well as future tasks.
Our tool translates OWL 2 DL to TPTP. The TPTP syntax [
The OWL 2 Direct Semantics distinguishes between the object domain and the (disjoint) data domain. The object domain is the extension of owl:Thing; individuals are elements and classes are subsets of the object domain. The data domain is the extension of rdfs:Literal; literals are elements and datatypes are subsets of the data domain. Thus, one natural way to translate OWL 2 DL to FOL is to use a typed first-order logic, and to treat owl:Thing and rdfs:Literal as diferent types. An alternative approach is to use untyped FOL, to treat owl:Thing and rdfs:Literal as unary predicates and to introduce axioms that capture the information that would otherwise be represented by the type system. TPTP provides formats for both typed and untyped FOL. Since the untyped fof-format is supported by a wider range of FOL reasoners, we decided to use the second approach and translate OWL 2 formulae into the untyped fof-TPTP.
For our translation, we have defined a mapping [ ] which maps OWL 2 DL axioms and OWL expressions that are part of axioms to sets of FOL expressions. It has two parameters , , which are used to keep track of substitutions that need to be made. When the translation function is called on an axiom, the parameters are empty, i.e. = = ∅. If a parameter is empty, we omit it and, for example, write [] instead of [].
∅
With this mapping, we have determined a translation for each type of OWL expression. The mapping can then be applied recursively in order to translate an OWL axiom that consists of several OWL expressions into a corresponding FOL expression or a set of such. E.g., OWL axioms of the form (, ) are translated with a FOL sentence ∀([] → []). In natural language this means, that, if is a subclass of , then every individual which belongs to class also belongs to class . Note that and themselves are not yet translated, but are OWL class expressions and we need to apply our translation function again using the parameter wherever a variable is required. The complete translation function can be found on the project’s wiki page1. For the sake of brevity we just illustrate it in this paper with a short example:
[ ( ℎ, (, (ℎ , )))] ⇔ ∀([ ℎ] → [ (, (ℎ , ))]) ⇔ ∀([ ℎ] → ([] ∧ [ (ℎ , )])) ⇔ ∀([ ℎ] → ([] ∧ ∃([ℎ ] ∧ [])) ⇔ ∀( ℎ() → (() ∧ ∃(ℎ (, ) ∧ ()))) As this example illustrates, the translation function is the result of a straightforward translation of the Direct Semantics into FOL. In this example we use both substitution parameters, since a second variable is needed to translate the existential restriction. For the purpose of translating OWL to FOL it is suficient to keep track of only two variables as parameters (as our translation function illustrates). This might be counter-intuitive, since SROIQ contains features beyond the two-variable fragment of FOL like, for example, transitivity axioms and counting quantifiers. However, the translation of these axioms only requires to use additional new variables, and does not require the reuse of more than two variables that have been introduced before. Therefore, two substitution parameters sufice.
An OWL ontology is translated to FOL by translating all of its axioms and adding some background axioms. Some of them axiomatise the distinction between objects and data in OWL and provide a kind of ‘soft-typing’ as discussed in Section 2. For example, for any class in the signature of the OWL ontology, a background axiom ∀(() → owl:Thing()) is added to the FOL translation. Other background axioms capture assumptions of the Direct Semantics (e.g., the extension of owl:Thing and rdfs:Literal are nonempty). A third kind of background axiom provides the axiomatisation for the OWL reserved vocabulary (e.g., ∀¬owl:Nothing()).
The structure of our implementation as shown in Figure 1 is based on the two tools we used,
namely the OWL API and Gavel. The OWL API is a Java toolkit to create, load and change
OWL ontologies. It represents the ontology as objects that can be traversed when working
with the ontology. It also provides access to OWL reasoners such as Hermit [
The goal of our tool is to translate OWL ontologies into first order logic. This means both the OWL tools of the OWL API and the FOL tools of Gavel provide important functionality for FOWL. Because the OWL API is only available in Java and Gavel only in Python, FOWL uses both languages. FOWL is started and stopped from Python. The Python script then starts a Java server that handles the OWL ontology and communicates with Python via Py4J 3.
When the Python script starts the Java server, it specifies as a parameter the ontology which is to be translated. This can be a local file or an IRI. The ontology then gets loaded by the OWL API, along with any imported ontologies. The visitor pattern, an easy and eficient way to visit each object of the ontology, is used to traverse recursively through the ontology and create the FOL translation. The translation is then saved in classes that mirror Gavel’s FOL classes and can be identified by their name function. These classes are provided to the Python script, which iterates through the sentences provided by the Java server and translates them in a 1:1 style to the appropriate Gavel classes. For reasoning over the translation, the sentences are then parsed into the TPTP format.
By providing a text file with conjectures in TPTP format, the VAMPIRE reasoner can then reason over those conjectures. Gavel provides access to the reasoning result, as well as the steps leading to it. The proof status is classified by using the SZS ontologies 4.
FOWL can be accessed via a command line interface. It features functions that translate ontologies and provide access to OWL reasoner Hermit as well as FOL reasoners VAMPIRE and E. More detailed instructions on how to install and use FOWL can be found on the project’s Github page 5. FOWL can be used according to the GNU Afero General Public License.
Performance We evaluated the performance of FOWL for translating diferent OWL
ontologies to TPTP. The ontologies are Basic Formal Ontology (BFO) [
The results are shown in Figure 2. BFO and the Pizza Ontology, which are the smallest ontologies in our evaluation, have a significantly higher time-per-axiom-ratio than the larger ontologies. This is possibly a result of the overhead due to background axioms and function calls which is unafected by the ontology size. Figure 2b also shows that strongly axiomatized ontologies such as OBI do not lead to a significant performance loss compared to weakly
(a) Absolute performance (b) Relative performance axiomatized ontologies. This implies that the type of axioms does not have a big influence on the translation performance.
Consistency If FOWL’s translation is correct, it should preserve the (in)consistency of an ontology across the translation. Thus, in order to evaluate the quality of the translation of FOWL, we ran the following experiment: We created a set of consistent and a set of inconsistent OWL ontologies, translated them with FOWL to FOL, and evaluated the consistency of the result using VAMPIRE.
For this purpose we extracted modules of ChEBI based on randomly chosen classes using ROBOT 7. Since ChEBI is consistent, all of its modules are consistent. In our experiment we considered 168 consistent ontologies. To create inconsistent ontologies, we used modules of ChEBI as starting point, but added additional axioms that lead to an inconsistency. For this purpose an OWL reasoner was utilised to classify a given ChEBI module, and a random theorem was selected for the purpose of generating a contradiction. E.g., if for a given ChEBI module a theorem Subclass(, ) was selected, then the ontology consisted of the original ChEBI module plus axioms asserting an individual that instantiates , but not . (Disjointness was used analogously.) Using this approach 1261 inconsistent ontologies were created. Thus, the experiment involved 1429 ontologies. In all cases VAMPIRE evaluation of the consistency of the translated ontology matched the original OWL ontology.
In conclusion, the conducted experiments support that consistency of an ontology is preserved across the translation.
FOWL translates OWL 2 DL axioms into first-order axioms in TPTP format [
The Heterogeneous Tool Set, Hets, supports the translation of OWL 2 DL ontologies into
FOL theories in various a number of formats including TPTP [
Enabling the translation of OWL ontologies into rfist order logic gives ontology designers the ability to combine the strengths of both languages. The OWL language is relatively easy to use and is well supported by tools, thus it has been widely adopted for ontology engineering projects. Nevertheless, it is common that nuances and axiomatic complexities of domain knowledge can remain outside the reduced expressiveness of OWL as compared to the full FOL. The presented tool can translate OWL ontologies into FOL in order to enable modular addition of and reasoning with FOL-native axioms.
The tool allows export of the translation result in TPTP syntax. Additional conjectures can then be added, using TPTP syntax, to be reasoned over in combination with the translation, and the ontology can be checked for consistency both in OWL and in FOL. FOWL has been tested on diferent ontologies and has been shown to preserve the consistency properties of ontologies during translation.
Further work will include improving the performance of the tool as well of adding features of convenience. For example, currently the predicate symbols of the FOL translations are based on the IRIs in the OWL file. This works well for ontologies that use meaningful IRIs, but is inconvenient for ontologies that use alphanumeric IRIs as class and property names.Hence, we are planning to provide an option that uses a given annotation property (like rdfs:label) for the generation of predicates. In addition, we will define a vocabulary for annotating OWL ontologies with FOL axioms. FOWL will recognise these annotations and enrich the OWL translation with these additional FOL axioms.
Although, in general, FOL model finders do not scale well, the performance may be
significantly increased by techniques like optimal definition elimination [