Relative Complexities of First Order Calculi von Elmar Eder | ISBN 9783528051228

Relative Complexities of First Order Calculi

von Elmar Eder
Buchcover Relative Complexities of First Order Calculi | Elmar Eder | EAN 9783528051228 | ISBN 3-528-05122-1 | ISBN 978-3-528-05122-8

Relative Complexities of First Order Calculi

von Elmar Eder

Inhaltsverzeichnis

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