Logic and Computation advanced course:
Reasoning in complex theories and applications.
Teacher
Course material: sofronie-lecture-esslli-09.pdf
Abstract:
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
representation.
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.