Relative Complexities of First Order Calculi: Künstliche Intelligenz

1 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.