Automated Reasoning via Multi-Sorted Fragment of Computable Set Theory

Computable Set Theory is a research field rich of interesting theoretical results, in particular for multi-sorted and multi-level syllogistic fragments, useful to provide novels powerful knowledge representation and reasoning frameworks for the Semantic Web. This book, which presents the author's doctoral dissertation, shows the application of a syllogistic fragment of computable set theory called 4LQSR for representing and reasoning on expressive decidable Description Logics (DLs) used to represent ontological knowledge via Semantic Web technologies. 4LQSR permits to represent expressive DLs and provides a unique formalism which combines the features of DLs with rule languages. These features are exploited to represent a novel Web Ontology Language (OWL) 2 profile, and hence as reasoning framework for a large family of ontologies. Then, the most widespread reasoning tasks concerning the represented DLs are also studied together with their decidability. Finally, the book presents a correct and terminating algorithm for those problems, based on the KE-tableau system, a refutation system inspired to the Smullyan's semantic tableaux, providing also computational complexity results.

Autorentext
Daniele Francesco Santamaria holds a post-doctoral position at the Department of Mathematics and Computer Science of the University of Catania in Italy. He is also contract professor for the same university. His research interests range from Semantic Web, both from a practical and theoretical perspective, to software and algorithm engineering.