Formal Foundations of Ontologies and Reasoning
Course taught at the Spring School on Linked Data and the Semantic Web for Humanities research (LiSeH 2019), in Graz, Austria, on 26 April 2019.
This course provides an introduction to Description Logics (DLs), a family of logic-based knowledge representation formalisms with interesting computational properties and a variety of applications. It turns out DLs are well-suited for representing and reasoning about terminological knowledge and constitute the formal foundations of semantic-web ontologies. There are different flavours of description logics with specific expressive power and applications, an example of which is ALC and on which we shall have a strong focus in this course. We start by motivating the need for formal foundations in the specification of and reasoning with ontologies. We then present the description logic ALC, its syntax, semantics, logical properties and proof methods, especially the tableau-based one. Finally, we illustrate the usefulness of DLs with the popular Protégé ontology editor, a tool allowing for both the design of DL-based ontologies and the ability to perform reasoning tasks with them.