Relative complexities of first order calculi

Inhaltsverzeichnis1 Calculi for First Order Logic.1.1 Basic Concepts and General Remarks.1.2 Resolution.1.3 The Connection Method.1.4 Consolution.1.5 The Tableau Calculus TC.1.6 The Sequent Calculus.1.7 Natural Deduction.1.8 A Frege-Hilbert Calculus.2 Comparison of Calculi for First Order Logic.2.1 Known Results on the Complexity of Calculi.2.2 Transformation to Clausal Form.2.3 Complexity Measures for Resolution Refutations.2.4 Simulation of the Connection Calculus by Resolution.2.5 Non-Simulatability of Resolution in the Connection Calculus.2.6 Variants of the Tableau Calculus TC.2.7 The Method of Tableaux and the Connection Method.3 The Extension Rule in First Order Logic.3.1 The Extension Rule.3.2 Complexities of Formulas and Derivations.3.3 Occurrences in the Sequent Calculus.3.4 Application of Substitutions to Formulas.3.5 Transformation of Sequents to Clauses.3.6 Simulation of the Sequent Calculus in Extended Resolution.3.7 Gentzen’s Transformations.3.8 Definitions.4 Connection Structures.4.1 Unifier Sets.4.2 From Resolution to Connection Proofs.4.3 Connection Structures.4.4 The Connection Structure Calculus.4.5 Splitting with Connection Structures.4.6 Extended Definitional Calculi.Conclusion.