Abstract

The main goal of this thesis is to propose an algorithm which bit by bit describes proofs of a particular set of tautologies in a certain proof system for propositional logic. In particular, we will study tautologies formalizing the pigeonhole principle (PHP). These tautologies have short proofs in usual Frege proof systems, but there is no short proof in the resolution proof system. However, there is a possibility how to "implicitly" describe a long resolution proof by a polynomial-time algorithm. In addition, our construction allows to prove the soundness of the algorithm without proving PHP first. This can be used for formulation of stronger proof system than resolution itself. As it will be described in the following chapters, the existence of proof systems with short proofs is tightly connected with fundamental questions in complexity theory and the study of strong proof systems can help us in understanding these questions.

Keywords:
Implicit propositional proof, pigeonhole principle.

Table of Contents

Chapter 1 Introduction
    1.1 Notation
    
Chapter 2 Proof systems for propositional logic
    2.1 Propositional logic
        2.1.1 Syntax
        2.1.2 Semantics
    2.2 Propositional proof systems
    2.3 Frege proof systems
    2.4 Resolution
        2.4.1 Language
        2.4.2 Inference rules
        2.4.3 Soundness and completeness
    2.5 The strength of proof systems

Chapter 3 The pigeonhole principle
    3.1 Definition
    3.2 Proofs
        3.2.1 Overview
        3.2.2 Metaproof
        3.2.3 Resolution proof
    3.3 P-tree & DFS
        3.3.1 p-tree description
        3.3.2 Addressing
    3.4 Detailed description of the p-tree
    3.5 Alg-ip 
        3.5.1 Outline of alg-ip

Chapter 4 Soundness and complexity demands
    4.1 Relation to implicit proofs
    4.2 Complexity demands
        4.2.1 General estimates
        4.2.2 alg-ip
    4.3 Soundness