A Proof Theory for Description Logics
Description Logics (DLs) is a family of formalisms used to represent knowledge of a domain. They are equipped with a formal logic-based semantics. Knowledge representation systems based on description logics provide various inference capabilities that ded
- PDF / 127,442 Bytes
- 7 Pages / 439.37 x 666.142 pts Page_size
- 27 Downloads / 210 Views
Introduction
Abstract Description Logics (DLs) are quite well-established as underlying logics for Knowledge Representation (KR). In a broader sense, a Knowledge Base (KB) specified in any description logic is called an Ontology. In this book, we are not interested in the technological concerns around Ontologies. For us, a DL theory, that is, a set of axioms in the DL logical language, and, an OWL file containing the same set of axioms is the same KB. Research in DL, since the beginning, was oriented to the development of systems and to their use in applications. Despite the higher efficiency of the recent available DL systems they do not provide to ontology engineers a good support for explanations of entailments like answering whether a subsumption holds or not, query or classification of concepts and roles of an ontology. This book is our first step in the direction of contract deduction systems with better explanation support. Keywords Description logic · ALC · Deduction system explanation · Sequent calculus · Natural deduction
· Proof theory · Proof
1.1 Description Logics Description Logics (DLs) are quite well-established as underlying logics for Knowledge Representation (KR). Part of this success comes from the fact that it can be seen as one (logical) successor of Semantics Networks [28], Frames [25] and Conceptual Graphs [38] and as well as, an elegant and powerful restriction of FOL by guarded prefixes, that also leads to a straight interpretation into the K propositional modal logic. The core of the DLs is the ALC description logic. In a broader sense, a Knowledge Base (KB) specified in any description logic having ALC as core is called an Ontology. In this book we will not take any ontological1 discussion on the choice for this terminology by the computer science community. Moreover, we are not inter1
In the philosophical sense.
A. Rademaker, A Proof Theory for Description Logics, SpringerBriefs in Computer Science, DOI: 10.1007/978-1-4471-4002-3_1, © The Author(s) 2012
1
2
1 Introduction
ested in the technological concerns around Ontologies, the Web or the fact that there is an XML dialect for writing Ontologies, just named OWL [14]. For us, a DL theory presentation, that is, a set of axioms in the DL logical language, and, an OWL file containing the same set of axioms is the same KB. Description Logics is a family of formalisms used to represent knowledge of a domain. In contrast with other knowledge representation systems, Description Logics are equipped with a formal, logic-based semantics. This logic-based semantics provides to systems based on it various inference capabilities to deduce implicit knowledge from the explicitly represented knowledge.
1.2 Motivation Research in DL, since the beginning, was oriented to the development of systems and to their use in applications. In the first half of the 1980’s several systems were developed including KL-ONE [6] and KRYPTON [5], only to mention two. They were called first generation DL systems. Later, in the second half of 1980’s, the second
Data Loading...
