Automated Reasoning via a Multi-sorted Fragment of Computable Set Theory with Applications to Semantic Web

In this dissertation, we investigate both theoretical and practical aspects of automated reasoning, focusing on the context of semantic web and ontology engineering.
In the first part of the dissertation, we consider some results of computable set theory, a research field rich of several decidability results for multi-sorted and multi-level syllogistic fragments, that allow one to provide a novel powerful knowledge representation and reasoning framework for the semantic web. For this purpose, we use a multi-sorted set-theoretic fragment called 4LQSR, admitting variables of four distinct sorts and a restricted form of quantification, to represent and reason on expressive decidable description logics (DLs). Specifically, we show that 4LQSR allows one to represent both the description logic DL4xD, which defines a novel Web Ontology Language (OWL) 2 profile, and an extension of the Semantic Web Rule Language (SWRL) admitting full negation and disjunction.
Then, we study the most widespread reasoning tasks concerning DL4xD-TBoxes and DL4xD-ABoxes, and we solve them by exploiting correct and terminating algorithms based on the KE-tableau system, a refutation system inspired to the Smullyan’s semantic tableaux. We also provide computational complexity results for such procedures.
Finally, we describe a C++ implementation of such algorithms admitting ontologies serialized in the OWL/XML format.
In the second part of the dissertation, we develop some semantic web ontologies to address problems concerning the fields of georeferencing and human and social sciences.
Specifically, we introduce the following three ontologies.
The first one, called OntoLocEstimation, is an ontology representable in DL4xD. It has been conceived for recognizing location names in non-structured texts and to handle data and reason about them, even in presence of name ambiguities.
The second ontology, called ArchivioMuseoFabbrica, is also representable in DL4xD. It has been introduced to study the history of the renovation of the Benedictine Monastery of San Nicolò L’Arena in Catania by the architect Giancarlo De Carlo, the arrangement of the areas of the building, the people involved, and the social events occurred during such process of renovation, which lasted 28 years (1977-2005).
The latter ontology, called SaintGall, is intended to study the shape of an ideal Benedictine monastery and the peculiarities that identify and distinguish it from other religious buildings. It has been defined by analyzing the Saint Gall map, one of the most ancient descriptions of a Benedictine monastery. The ontology SaintGall can be considered as a first step towards the definition of the architectonic type of monastery.