When one Logic is Not Enough Integrating First-order Annotations in OWL Ontologies Simon Flügel1 Martin Glauer1 Fabian Neuhaus1 and Janna

2025-04-29 0 0 759.7KB 22 页 10玖币

侵权投诉

When one Logic is Not Enough: Integrating

First-order Annotations in OWL Ontologies

Simon Flügel1, Martin Glauer1, Fabian Neuhaus1, and Janna

Hastings2,3

1Institute for Cooperating Systems, Otto von Guericke University

Magdeburg, Germany

2Faculty of Medicine, Institute for Implementation Science in

Health Care, University of Zurich, Switzerland

3School of Medicine, University of St Gallen, Switzerland

October 10, 2022

Abstract

In ontology development, there is a gap between domain ontologies

which mostly use the web ontology language, OWL, and foundational on-

tologies written in ﬁrst-order logic, FOL. To bridge this gap, we present

Gavel, a tool that supports the development of heterogeneous ’FOWL’

ontologies that extend OWL with FOL annotations, and is able to reason

over the combined set of axioms. Since FOL annotations are stored in

OWL annotations, FOWL ontologies remain compatible with the existing

OWL infrastructure. We show that for the OWL domain ontology OBI,

the stronger integration with its FOL top-level ontology BFO via our ap-

proach enables us to detect several inconsistencies. Furthermore, existing

OWL ontologies can beneﬁt from FOL annotations. We illustrate this

with FOWL ontologies containing mereotopological axioms that enable

new meaningful inferences. Finally, we show that even for large domain

ontologies such as ChEBI, automatic reasoning with FOL annotations can

be used to detect previously unnoticed errors in the classiﬁcation.

1 Introduction

The landscape of applied ontology contains a rift. The vast majority of ontolo-

gies that are used in computational systems are written in OWL, more speciﬁ-

cally OWL 2 DL or OWL language proﬁles, which are essentially sublanguages

of OWL 2 DL.1However, the authors who work on the foundational topics of

1In the following we will for the sake of brevity refer to OWL 2 DL and OWL 2 language

proﬁles as ‘OWL’. We are aware of so-called ‘OWL 2 Full’ (i.e., OWL 2 without DL constraints

and a RDF-based semantics), but since it is rarely used, we will not consider it in this paper.

arXiv:2210.03497v1 [cs.AI] 7 Oct 2022

applied ontology, such as upper level entities and their axiomatisations, typically

do not use OWL. E.g., in 2020 and 2021 the Formal Ontology in Information

Systems conferences accepted altogether 19 papers on foundational topics. Of

those, none used OWL as representational language.

The reason for this language rift is easy to explain. The OWL Manchester

Syntax is relatively easy to learn for domain experts, and there are an increas-

ing number of widely available tools supporting development of ontologies in the

OWL language. Furthermore, OWL is based on the description logic SROIQ

and, thus, satisﬁability of OWL ontologies and logical inference with OWL on-

tologies are decidable decision problems. Both factors are major advantages

for anybody who develops a domain ontology in cooperation with domain ex-

perts and intends to use automatic reasoning (e.g., using consistency checks

for quality control). However, the advantages come with a price: in order to

improve readability and achieve decidability one needs to sacriﬁce expressivity.

Consequently, many ontological diﬀerences that are studied by foundational

ontologists are not expressible in OWL. E.g., part-whole relationships are a

staple of most ontologies and have been extensively studied by foundational on-

tologists. However, in OWL 2 DL it is even impossible to axiomatise proper

parthood as strict order, let alone represent interesting distinctions between dif-

ferent mereologies [16]. Hence, foundational ontologists typically use ﬁrst-order

logic (FOL) or even more expressive logics as representational languages. Con-

sequently, the vast majority of papers on foundational ontology contain axioms

and deﬁnitions that cannot be directly reused by the ontologies that are used

in practice in information systems. The language rift thus prevents theoretical

results and insights from achieving their full impact in beneﬁting downstream

practical applications.

A particularly interesting case are upper level ontologies, which aim to pro-

vide a reusable framework for the development of domain ontologies. There are

a number of diﬀerent upper level ontologies [4], which reﬂect a wide range of

philosophical points of view. Most widely used is the Basic Formal Ontology

(BFO), which is used by more than 250 ontology projects. BFO is grounded

in a rich Aristotelian tradition, is described in numerous publications, a user

guide, and a textbook, and most recently it has even been standardised by the

International Organization for Standardization as ISO/IEC 21838-2:2021. How-

ever, the version of BFO that is actually used in most information systems is

BFO 2.0 OWL, which contains exactly 52 axioms, more precisely 18 disjointness

axioms and 34 subsumption axioms between atomic classes. Interestingly, BFO

2.0 OWL contains annotations that include additional axioms in the Common

Logic Interchange Format (CLIF), a variant of FOL2, which provide a much

richer logical axiomatisation than the OWL axioms. However, since OWL rea-

soners ignore annotations, these axioms are computationally inert; they only

serve as documentation for the human readers. In summary, while there is a

rich literature on BFO, almost none of it is materialised in the format that is

2Technically, Common Logic is more expressive than FOL [7], but for the purpose of this

paper the diﬀerences may be ignored.

actually used by domain ontologies. From a logical point of view BFO 2.0 OWL

is just a simple taxonomy with a few additional disjointness axioms. Conse-

quently, the developers of domain ontology cannot use OWL reasoners or other

automatic reasoners to check whether their ontology actually conforms to BFO.

The goal of this paper is to present Gavel 3and its OWL-speciﬁc extension

Gavel-OWL 4, tools that were developed to bridge the language rift by enabling

ontology developers to develop heterogeneous ontologies that contain both FOL

and OWL axioms, and supports reasoning with the integrated model. One

major beneﬁt of Gavel and Gavel-OWL is that it does not require developers of

applied ontologies to make any changes to their established workﬂow for OWL

ontologies: developers can continue to use the same tools (e.g., Protégé) to

develop their ontologies, and use standard OWL reasoners to reason with the

OWL part of the ontology. Gavel-OWL merely oﬀers the additional option to

enhance an OWL ontology with FOL axioms. These additional axioms may be

based on a foundational ontology, but they may also be domain speciﬁc axioms

that are expressible in FOL but not in OWL.

In section 2 that follows, we discuss the requirements for Gavel-OWL and

our approach for addressing them. The capabilities of Gavel-OWL and its im-

plementation are presented in section 3. Afterwards, we discuss in section 4

the merits of the approach by ﬁrst showing how Gavel-OWL overcomes some

limitations of OWL that have been discussed in the literature, and then we con-

sider two case studies. In the ﬁrst, we will show that BFO CLIF axioms may be

used to ﬁnd errors in an BFO-based OWL domain ontology. In the second, we

extend a large domain ontology with FOL axioms and illustrate how automatic

theorem proving with the heterogeneous ontology yields new subsumptions that

an OWL reasoner on its own is not able to detect. In the remainder of the paper

we discuss related work, the signiﬁcance and potential impact of the approach.

2 Requirements and Approach

Our goal is to enable ontology developers to beneﬁt from the advantages of

OWL, including its user friendly syntax, decidability, and mature tool chain,

without having to forego the ability to use the greater expressivity of FOL

when it is required, or when a preexisting FOL ontology is available.

Thus, a FOWL ontology consists of two components, an OWL component

and a FOL component, which extends the OWL axioms with additional axioms

in FOL. To achieve this goal our solution ideally should meet the following

requirements:

1. In order to remain accessible by the existing OWL infrastructure, FOWL

ontologies should be syntactically valid OWL ontologies.

2. The OWL component of a FOWL ontology should be usable by existing

OWL tools and follow the OWL 2 DL semantics as speciﬁed in [14].

3https://github.com/gavel-tool/python-gavel

4https://github.com/gavel-tool/python-gavel-owl

Figure 1: View of an annotated OWL entity in Protégé.

3. For convenience of editing and debugging, it should be possible to associate

FOL axioms closely with related OWL entities and axioms. Ideally, this

should be able to be done with tools like Protégé, which are widely used

for ontology editing.

4. In addition, it should be possible to integrate existing FOL ontologies

(e.g., a foundational ontology) with a FOWL ontology.

5. Automatic reasoning with an FOWL ontology should utilise both its OWL

and its FOL axioms.

Our approach for meeting these requirements is to create a combined OWL

and FOL ontology through annotations in OWL ontologies. Thus, in some

sense we follow the precedent set by BFO 2.0 OWL, which is also an OWL

ﬁle that contains FOL annotations. However, while in BFO 2.0 OWL the FOL

annotations are logically inert, Gavel-OWL enables automatic reasoning with

the logical theory that is the result of combining the OWL axioms with the FOL

axioms.

More speciﬁcally, a FOWL ontology is an OWL ﬁle, where one or multiple

annotation properties are selected, and all values of AnnotationAssertion axioms

with these annotation properties are interpreted as FOL axioms. Hence, the

heterogenous ontology is represented in a syntactically valid OWL ﬁle and the

OWL part of the ontology may be processed by standard OWL tools, because

the FOL annotations do not inﬂuence the ontology’s OWL semantics.

As they are stored in annotation values, the FOL axioms also remain closely

connected to the OWL axioms: typically, all axioms for a given subject entity

are grouped together. For instance, Figure 1 shows how Protégé displays anno-

tations and logical OWL axioms for the entity proper part of. The FOL axioms

can be seen in the upper part and the OWL axioms in the lower part. Thus, a

user is able to view related FOL and OWL axioms on the same screen.

Gavel-OWL supports two diﬀerent syntaxes for FOL annotations: CLIF

and TPTP. CLIF is a human readable syntax for ISO Common Logic [7].5The

TPTP syntax is widely used in the automatic theorem proving community, in

particular the TPTP problem library [30, 29]. To increase the readability of

TPTP, we do not use complete TPTP axioms, but only their formula part.

E.g., we write

![X] ~ ’proper part of’ (X,X)

instead of the full TPTP expression

fof(axiom_name, axiom, (![X] ~ ’proper part of’ (X,X))).

Reasoning with a FOWL ontology requires the integration of its OWL com-

ponent with its FOL component. This is done by translating the OWL axioms

into FOL (in TPTP syntax) and integrating them with the FOL axioms from

the annotations6as well as, potentially, additional axioms from a background

theory. The result is a FOL ontology in TPTP syntax, which can be used for

automatic reasoning and consistency checking. To enable these automated con-

sistency checks, Gavel is able to interact with the theorem prover Vampire [18].

Furthermore, Gavel features a dynamic extension scheme that allows for the

integration of other logics through new plugins. We present here Gavel-OWL,

which allows the integration of ﬁrst-order logic and OWL. Other ontologies may

also use logics for annotation, such as typed logics or higher order logics. These

can then be connected to Gavel by separate plugins similar to Gavel-OWL and

to use the same proof pipelines described in this submission.

One obstacle for the integration of OWL axioms and FOL annotations is

that it is necessary to map their signatures. E.g., in the example in Figure 1

an OWL entity, more speciﬁcally an object property, is annotated with a CLIF

axiom. The OWL and the FOL axioms together specify proper parthood as

strict partial order. (This could not be axiomatised in OWL 2 DL, since the

axiom would violate its global restrictions.) However, strictly speaking, the

OWL axioms are about the entity uniquely identiﬁed by a long IRI (namely,

http://purl.obolibrary.org/obo/BFO_0000175) , which is then annotated

with the literal ’proper part of’^^xsd:string as label, while the CLIF axioms

are using neither the OWL IRI nor the exact label of the OWL entity, but

the CLIF name “proper_part_of". This is indicative of a typical problem.

IRIs are often too long to be conveniently typed by human. Thus, one cannot

expect the FOL annotations to include the complete IRIs that are used to

identify an OWL entity. Further, following recommended best practices [20],

5Strictly speaking, CLIF’s syntax is more ﬂexible than ‘normal’ FOL because it does not

distinguish between individual constants, predicate and function symbols. In addition, CLIF

includes sequence variables which increase the expressiveness of CLIF beyond FOL. However,

for the purpose of this paper we treat CLIF just as an alternative syntax for ‘normal’ FOL.

6CLIF axioms are also translated into TPTP syntax.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

WhenoneLogicisNotEnough:IntegratingFirst-orderAnnotationsinOWLOntologiesSimonFlügel1,MartinGlauer1,FabianNeuhaus1,andJannaHastings2,31InstituteforCooperatingSystems,OttovonGuerickeUniversityMagdeburg,Germany2FacultyofMedicine,InstituteforImplementationScienceinHealthCare,UniversityofZurich,Switzerla...

展开>> 收起<<

When one Logic is Not Enough Integrating First-order Annotations in OWL Ontologies Simon Flügel1 Martin Glauer1 Fabian Neuhaus1 and Janna.pdf

共22页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

When one Logic is Not Enough Integrating First-order Annotations in OWL Ontologies Simon Flügel1 Martin Glauer1 Fabian Neuhaus1 and Janna

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: