Towards a Theory of Proofs of Classical Logic

The questions What is a proof? and When are two proofs the same? are fundamental for proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we still have no satisfactory answers. This is embarrassing not only for proof theory itself, but also for computer science, where classical propositional logic plays a major role in automated reasoning and logic programming. Also the design and verification of hardware is based on classical Boolean logic. Every area in which proof search is employed can benefit from a better understanding of the concept of proof in classical logic, and the famous NP-versus-coNP problem can be reduced to the question whether there is a short (i.e., polynomial size) proof for every Boolean tautology. Usually proofs are studied as syntactic objects within some deductive system (e.g., tableaux, sequent calculus, resolution, ...). Here we take the point of view that these syntactic objects (also known as proof trees) should be considered as concrete representations of certain abstract proof objects, and that such an abstract proof object can be represented by a resolution proof tree as well as by a sequent calculus proof tree, or even by several different sequent calculus proof trees. The main theme of this work is to get a grasp on these abstract proof objects, and this will be done from three different perspectives, studied in the three parts of this thesis: abstract algebra (Chapter 2), combinatorics (Chapters 3 and 4), and complexity (Chapter 5).