Relative Complexities of First Order Calculi

ISBN-13: 9783528051228 / Angielski / Twarda / 1992 / 180 str.

Elmar Eder

Opis

In this paper, a comparison is made of several proof calculi in terms of the lengths of shortest proofs for some given formula of first order predicate logic with function symbols. In particular, we address the question whether, given two calculi, any derivation in one of them can be simulated in the other in polynomial time. The analogous question for propositional logic has been intensively studied by various authors because of its implications for complexity theory. And it seems there has not been as much endeavour in this field in first order logic as there has been in propositional logic. On the other hand, fOr most of the practical applications of logic, a powerful tool such as the language of first order logic is needed. The main interest of this investigation lies in the calculi most frequently used in automated theorem proving, the resolution calculus, and analytic calculi such as the tableau calculus and the connection method. In automated theorem proving there are two important aspects of complexity. In order to have a good theorem proving system, we must first have some calculus in which we can express our derivations in concise form. And second, there must be an efficient search strategy. This book deals mainly with the first aspect which is a necessary condition for the second since the length of a shortest proof always also gives a lower bound to the complexity of any strategy.

Spis treści

1 Calculi for First Order Logic.- 1.1 Basic Concepts and General Remarks.- 1.1.1 First Order Predicate Logic.- 1.1.2 Substitutions and Unification.- 1.2 Resolution.- 1.3 The Connection Method.- 1.3.1 The Connection Method in Propositional Logic.- 1.3.2 The Connection Method in First Order Predicate Logic.- 1.3.3 Splitting.- 1.4 Consolution.- 1.4.1 Consolution in propositional logic.- 1.4.2 Consolution in first oder logic.- 1.4.3 Simulation of resolution and connection calculus by 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.6.1 The Tableau Calculi T Cac, TCiac and TCm.- 2.6.2 Comparison of Tableau Calculi.- 2.6.3 The Tableau Calculus with Unification, TCu.- 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.5.1 The Definition Set for a Derivation in the Sequent Calculus.- 3.5.2 Transforms.- 3.5.3 Equivalence of Transforms.- 3.5.4 Inheritance of Transforms.- 3.6 Simulation of the Sequent Calculus in Extended Resolution.- 3.6.1 Tree Derivations.- 3.6.2 Arbitrary Derivations.- 3.7 Gentzen’s Transformations.- 3.7.1 Simulation of the Frege-Hilbert Calculus in Natural Deduction.- 3.7.2 Simulation of Natural Deduction in the Sequent Calculus.- 3.7.3 Simulation of the Sequent Calculus in the Frege-Hilbert Calculus.- 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.