On the Notion of Efficiency of Formal Systems from the Point of View of Inference Search Problems
by
Alexandre Lyaletsky, Jr.
Faculty of Cybernetics, Kyiv National Taras Shevchenko University, Kiev, Ukraine

This paper is mostly devoted to consideration of two tasks.

In the first place, some investigations are made for such preorder relations over sets of calculi that can be considered as relations simulating relations of efficiency from the point of view of the problems of efficient computer-oriented logical inference search. For this, in particular, the notion of a ``locally given preorder relation'' can be introduced by using the category language. We can attempt to construct a general theory of these relations, which contains, for example, the problem of reduction of the investigation of such a relation to the investigation of another one. (The notion of ``density'' for partially ordered sets could be useful for solving the problem of reduction.) But in this paper we restrict us mainly by the consideration of one special class of locally given relations, namely by so-called relations of E_\Sigma-efficiency (\Sigma denotes a category which serves as a basis for the construction of E_\Sigma). The reason for this is the fact that these relations are suitable for simulating the notion of efficiency in the sense given above. It is shown that investigating ``classical'' locally given relations that order considered calculi in accordance with a length of inference search can be reduced to investigating relations E_\Sigma.

In the second place, some investigations of possibility of the construction of such a constructive partial operation that every constructive calculus transforms into more E_\Sigma-effective calculus and that satisfy some additional requiments. Necessary and sufficient conditions of the existence of these ``effectiveness-giving'' operations for so-called logical \alpha-categories are found, where logical \alpha- categories are categories corresponding to logics in a certain sense. The great meaning concerning this question has an operation \biguplus satisfying the following properties:

1. Let \Sigma be a logical \alpha-category and partial algebras A and B be its objects, and besides A and B have the same signature. Then A E_\SigmaA\biguplusB and B E_\SigmaA\biguplusB.

2. Let \Sigma be a logical \alpha-category and partial algebras A and B be its objects, and besides A E_\SigmaB. Then there exist such objects of \Sigma A' and B' that A ~ _\Sigma A' and A'\biguplus B' = B.

(In the property 2 the expression A ~ _\Sigma A' denotes that A and A' are E_\Sigma-equivalent.)

Results of this paper follow, in particular, that constructive calculi corresponding to classical and intuitionistic propositional logics have constructive ``effectiveness-giving'' operations. This fact permits to implement automated tools for constructing more and more effective classical and intuitionistic calculi. The author hopes to obtain analogous results for first-order logics.

Date received: April 30, 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-35.