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

Semantic Web is a vision of the web in which machine-readable data enables software agents to manipulate and query information on behalf of human agents. To achieve such goal, machines are provided with appropriate languages and tools. Investigating new technologies which can extend the power of knowledge representation and reasoning systems is the main task of my research work started by observing the lack of some desirable characteristics concerning the expressiveness of semantic web languages and their integration with some features of rule-based languages, arisen with the study of some application domain during the draft of my bachelor thesis. Specifically in this dissertation, I consider some results of \emph{Computable Set Theory}, a research field rich of several interesting theoretical results, in particular for what concerns multi-sorted and multi-level syllogistic fragments, in order to provide a novel powerful knowledge representation and reasoning framework particularly devoted to the context of Semantic Web. For this purpose, I use a syllogistic fragment of computable set theory called $\flqsr$, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, to represent and reason on expressive decidable \emph{description logics} (DLs) which can be used to represent ontological knowledge via Semantic Web technologies. I show that the fragment $\flqsr$ allows one to represent an expressive DL called $\dlss$ ($\shdlss$ for short) and its extension $\dlssx$ ($\shdlssx$ for short). The DL $\shdlssx$ admits, among other features, Boolean operations on concepts and roles, data types, and product of concepts. Moreover, $\flqsr$ provides a unique formalism which combines the features of the DL $\shdlssx$ with a rule language admitting full negation and subject to no safety condition. I show that $\flqsr$ can be used to represent a novel Web Ontology Language (OWL) 2 profile, and hence can be used as reasoning framework for a large family of ontologies. Then, I study the most widespread reasoning tasks concerning both $\shdlssx$-TBoxes and $\shdlssx$-ABoxes. In particular, I consider the \emph{Consistency Problem} of a $\shdlssx$-knowledge base (KB), the \emph{Conjunctive Query Answering} (CQA) for $\shdlssx$, which provides simple mechanism allowing users and applications to interact with data stored in the KB, and the \emph{Higher-Order Conjunctive Query Answering} (HOCQA) for $\shdlssx$, a generalization of the CQA problem admitting three sorts of variables, namely, individuals, concepts, and roles. The decidability of the above mentioned problems are proved by resorting them to analogous problems in the context of the set-theoretic language $\flqsr$ by means of a suitable mapping function from axioms and assertions of $\shdlssx$ to formulae of $\flqsr$. Then, I provide a correct and terminating algorithm for the HOCQA problem for $\shdlssx$ based on the \ke\space system, a refutation system inspired to the Smullyan's semantic tableaux, giving also computational complexity results. The algorithm also serves for the consistency problem of $\shdlssx$-KBs and for other reasoning tasks which the HOCQA problem can be instantiated to. I also introduce an implementation in C++ of the algorithm thus to provide an effective reasoner for the DL $\shdlssx$ which admits ontology serialized in the OWL/XML format.