Exploiting SAT and SMT Techniques for Automated Reasoning and Ontology Manipulation in Description Logics

Description Logics (DLs) are a family of logic-based knowledge representation formalisms aimed at representing the knowledge of an application domain in a structured way one of whose main characteristic is the emphasis on reasoning. Since the last two decades Description logics have been widely studied and applied to numerous areas of computer science (including artificial intelligence, formal verification, database theory, natural language processing and distributed computing). In recent years, however, the interest in the problem of automated reasoning in Description Logics has seen a tremendous growth because of the explosion of new notable applications in the domains of Semantic Web and of bio-medical ontologies. The more real-world problems are represented through DL-based ontologies the more these new applications represents a challenge due to the required efficiency in handling complex logical constructors (e.g. numerical constraints) and in handling the huge dimensions of this kind of ontologies. For these reasons the development of efficient algorithms and procedures for reasoning in Description Logic has become crucial. SAT-based technologies, in the meanwhile, proved to be mature and largely successful in many other automated reasoning fields, first of all on many very hard practical applications of formal verification, often huge characterized by problems of huge dimension. In the last twenty years, in fact, we have witnessed an impressive advance in the efficiency of SAT techniques, which has brought problems of hundreds of millions of clauses and variables to be at the reach of the freely-available state-of-the-art solvers. As a consequence, many problems have been successfully solved by mean of SAT-based techniques and these approaches are currently state-of-the-art in the respective communities (among all Model Checking). Furthermore, the progress in SAT-solving techniques, together with the concrete needs from real applications, have inspired significant research on richer and more expressive Boolean formalism, like Satisfiability Modulo Theories (SMT), and on the use of the SAT formalism to solve problems with a wider extent (e.g. to compute interpolants, unsatisfiable cores, all-SAT). The research trends in Description Logic, its manifold practical applications, the quest of efficient and scalable procedures, on one hand, the wide variety of mature and efficient techniques offered by the SAT research area, on the other hand, motivated our research. In this thesis dissertation we explore the idea of exploiting the power and efficiency of state-of-the-art SAT-based techniques for automated reasoning and ontology manipulation in Description Logics, proposing a convenient alternative to the traditional tableau based algorithms. With this aim we propose and develop novel and complete approaches able to solve Description Logic problems as SAT and SMT ones, by mean of sound and complete encodings. On these encodings we develop new procedures and optimizations techniques based on a variety of existing SAT-based formalisms and technologies. In this work, in particular, we focus on three gradually harder reasoning problems in Description Logics which tackle increasingly more expressive languages or increasingly harder reasoning services, among which we face also non-standard services supporting the debugging of ontologies like modularization and axiom pinpointing. We implemented our approaches in tools which integrate with the available SAT/SMT-solvers; finally, we show the effectiveness of our novel approaches through very extensive empirical evaluations on benchmarks and ontologies from real application, in which we compare our performance against the other state-of-the-art available systems. Notice that any advance in the exploited Boolean reasoning techniques/tools will be freely inherited from our proposed approaches extending also to Description Logics/ontologies the benefits of the observable great and fast advance in the efficiency of SAT-based techniques.