Tutorial affiliated with Tableaux ’17.
This page will contain resources and useful information for the tutorial once they are available.
Motivation and description
Traditionally, proof systems can be seen as nondeterministic algorithms for logics and theories, thus yielding upper bounds on nondeterministic complexity from bounds on proof size. The evolution of structural proof theory, however, has allowed us to see proof systems in a much finer way, obtaining better bounds by a more careful analysis of the proof search space. This includes methods for obtaining space bounds (e.g. via proof depth, loop checking) and co-nondeterministic time bounds (via invertible systems), in addition to the nondeterministic time bounds from the traditional approach.
Studying the complexity of decision algorithms induced by proof systems is useful not only for efficient proof search, but also conversely for the design of appropriate proof systems themselves. It is often the case that we know the complexity of a logic in advance, and this information can help provide intuitions for how the rules and lines of a corresponding proof system ought to look.Thus a working knowledge of proof search complexity is a powerful tool for students and researchers throughout the Tableaux community.
This tutorial will survey various methods of obtaining such complexity bounds for logics from proof systems, and present in detail several examples from the literature of how such methods can be applied to yield optimal bounds. We will also see how current trends in proof theory can be used to extract bounds, in particular highlighting the power of focussed and cyclic proofs to obtain alternating time bounds and deterministic space bounds, respectively.
This tutorial will assume no prior knowledge of computational complexity and aims to be accessible to students from all strands of the Tableaux community, assuming only a basic working knowledge of structural proof theory.