Note on effective constructibility of resolution proof systems. (English) Zbl 0790.03011
Eijck, Jan van (ed.), Logics in AI. European workshop JELIA ’90, Amsterdam, the Netherlands, September 10-14, 1990. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 478, 487-498 (1991).
The subject discussed in this paper is a part of a general problem of automated generation of resolution based proof systems for non-classical logics. In an earlier paper [the author, J. Exp. Theor. Artif. Intell. 3, 17-32 (1991; Zbl 0723.03004)], the class of resolution logics has been introduced and characterized. A resolution logic is a logical calculus whose refutational properties can be expressed in terms of the resolution principle. Resolution counterparts of resolution logics can be effectively constructed from semantic descriptions of these calculi. Such construction methods are called minimization algorithms and their purpose is to construct minimal resolution proof systems for resolution logics (minimal with respect to the number of premises of the resolution rule).
Resolution logics can be conveniently grouped into classes of logical calculi according to the criterion of having the same finite inconsistent sets. With every such class one can associate in a natural way two integers \(m>1\) and \(t>0\) such that the size of any resolution counterpart of any logic in the class is between \(m\) and \(m^{m^ t}\). For logics for which the size of a minimal resolution counterpart approaches \(m^{m^ t}\), general purpose minimization algorithms do not possess any practical value. Moreover, resolution counterparts of such sizes are too large to be efficiently implemented. It turns out that for many logical calculi the value of \(t\) is 1 and hence one may expect more efficient minimization algorithms for such logics. In the present paper we explore this direction; we consider minimization algorithms for resolution logics for which \(t=1\) and whose minimal resolution counterparts are ‘small’. The first class considered in this paper is the class of resolution logics which are, in a certain sense, functionally complete. Among functionally incomplete logics, Łukasiewicz finitely- valued logics (precisely \(n\)-valued logics where \(n-1\) is prime) possess the above properties and we present fast minimization algorithm for these logics.
For the entire collection see [Zbl 0768.00012].
Resolution logics can be conveniently grouped into classes of logical calculi according to the criterion of having the same finite inconsistent sets. With every such class one can associate in a natural way two integers \(m>1\) and \(t>0\) such that the size of any resolution counterpart of any logic in the class is between \(m\) and \(m^{m^ t}\). For logics for which the size of a minimal resolution counterpart approaches \(m^{m^ t}\), general purpose minimization algorithms do not possess any practical value. Moreover, resolution counterparts of such sizes are too large to be efficiently implemented. It turns out that for many logical calculi the value of \(t\) is 1 and hence one may expect more efficient minimization algorithms for such logics. In the present paper we explore this direction; we consider minimization algorithms for resolution logics for which \(t=1\) and whose minimal resolution counterparts are ‘small’. The first class considered in this paper is the class of resolution logics which are, in a certain sense, functionally complete. Among functionally incomplete logics, Łukasiewicz finitely- valued logics (precisely \(n\)-valued logics where \(n-1\) is prime) possess the above properties and we present fast minimization algorithm for these logics.
For the entire collection see [Zbl 0768.00012].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B50 | Many-valued logic |
