
×
Relative Complexities of First Order Calculi
von Elmar EderInhaltsverzeichnis
- 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.