Proof complexity is an interdisciplinary area of research utilizing techniques from logic, complexity, and combinatorics towards the main aim of understanding the complexity of theorem proving procedures. Traditionally, propositional proofs have been the main object of investigation in proof complexity. Due their richer expressivity and numerous applications within computer science, also non-classical logics have been intensively studied from a proof complexity perspective in the last decade, and a number of impressive results have been obtained.

The aim of this course is to present an up-to-date introduction to proof complexity with emphasis on non-classical logics and their applications. In particular, we will cover proof systems for modal logics, intuitionistic logics and non-monotonic reasoning. The course will introduce the relevant logics and explain in detail the proof systems associated with them. One of the main objectives in proof complexity is to obtain tight bounds on the size of proofs. In the course we will explain the method of feasible interpolation as one universal technique for proving lower bounds for the proof size. Feasible interpolation has been demonstrated for intuitionistic logic and a number of modal logics, which subsequently lead to exponential lower bounds for the proof size of combinatorial statements in these logics.

These proof-theoretic results will be complemented by illustrative examples showing the applicability of proof systems for non-classical logics to AI and automated theorem proving. Practitioners are not only interested in the size of a proof, but face the more complicated problem to actually construct a proof for a given instance. Thus we will discuss aspects of proof automatizability, proof search, and algorithms for satisfiability. The last two lectures will focus on proof complexity for non-monotonic logics. These are particularly interesting as non-monotonic aspects are now recognised as being rather important in various areas of KR that have previously been based on purely monotonic reasoning, such as DL reasoning for the Semantic Web or the Live Sciences. We will describe proof systems for default logic, autoepistemic logic, and circumscription, and also explain their relations to classical proof systems.

Pasted Graphic 1Pasted Graphic 5