Logic and Computation advanced course:
Reasoning in complex theories and applications.
Course material: sofronie-lecture-esslli-09.pdfAbstract:
The goal of this course is to give a comprehensive, in-depth
perspective on recent advances in the field of reasoning in
complex logical theories, and to present the applications of
these results in mathematics, formal verification and knowledge
We will start by explaining the importance of logical formalization in various areas (mathematics, verification, knowledge representation, AI). We will point out the limitations of the logic formalization, as well as the necessity of developing decision procedures. We will argue, using various examples, that concrete problems often are quite heterogeneous in nature, such that combinations of reasoning tools (resp. decision procedures) for various theories might be needed in the same application. We will introduce the necessary theoretical concepts and give a survey of decidable and tractable logical theories. We will then present recent achievements which address the main problems which occur in this context, starting from SAT checking in classical logic and continuing with tests of satisfiability modulo a theory, modular reasoning in combinations of theories (under various conditions on their shared signatures) and hierarchical reasoning in theory extensions. We will present the main ideas which appeared in the literature from a unifying perspective. We will illustrate the problems and the solutions on examples from mathematics, verification and knowledge representation.