On Efficient Quantifiers Manipulation in Gentzen's Calculi LK and LJ
by
Alexander Lyaletski
Faculty of Cybernetics, Kyiv National Taras Shevchenko University, Kiev, Ukraine

Investigations in computer-oriented reasoning gave rise to the appearance of various methods for the proof search in 1st-order logics. Particularly, Gentzen calculi [1, 2] can be used as a base for the construction of machine procedures for deduction without skolemization. But their practical application as logical inference technique for automated reasoning has not received wide use: preference is usually given to resolution-type methods. This is explained by higher efficiency of resolution-type methods as compared to Gentzen's calculi (e.g., LK and LJ) which mainly is connected with different possible orders of quantifier rule applications while resolution methods [3], due to skolemization, are free of this deficiency. (The question of construction of a modification of LK using preliminary skolemization was investigated in [4].)

When quantifier rules are applied, a substitution of selected terms for variables is made. To do this step of deduction sound, certain restrictions are put on the substitution. A substitution, satisfying these restrictions, is said to be admissible. Two main kinds of the notion of admissible substitutions can be extracted for sequent calculi: Gentzen's notion [1] and Kanger's notion [2].

In order to reach higher efficiency of sequent calculi in comparison with Gentzen's and Kanger's calculi including intuitionistic logic LJ, in this paper we show that use of certain modifications of the notion of admissible substitutions, which was introduced in [5], leads to optimizing quantifier rule applications in LK as well as in LJ and, as a result, to increasing the efficiency of inference search in modified calculi LK and LJ . This play a special role for LJ because application of skolemization for LJ requires sophistical technique of formulas transformation.

References: [1] Gentzen G. (1934) Untersuchungen uber das Logische Schliessen. Math. Zeit., 39, 176-210. [2] Kanger S. (1963) Simplified Proof Method for Elementary Logic. Computer Programming And Formal Systems, Studies in Logic. North-Holland Publ. Co., Amsterdam, p. 87-93. [3] Robinson J.A. (1965) A Machine-Oriented Logic Based on Resolution Principle. J. of the ACM, 12, 23-41. [4] Mints G. (1967) Herbrand Theorem (in Russian). Mathematical Theory of Logical Inference. Nauka, Moscow, 311-350. [5] Lyaletski A. (1981) A Variant of Herbrand Theorem for Formulas in the Prefix Form (in Russian). Kibernetika, 1, 112-116.

Date received: April 29, 2003

Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Mathematical Conference Abstracts. Document # cajy-34.