zbMATH — the first resource for mathematics

Gentzen-type systems and resolution rules. I: Propositional logic. (English) Zbl 0739.03011
Colog-88, Proc. Int. Conf., Tallinn/USSR 1988, Lect. Not. Comput. Sci. 417, 198-231 (1990).
[For the entire collection see Zbl 0709.00021.]
A resolution-type calculus is defined for propositional systems for which cut-free Gentzen formulations with the subformula property are known. These include intuitionistic logic and modal logic \(S4,S5,T,K4\) and \(K\). The basic idea is to generate a clause normal form by replacing complex subformulae in the skope of modal operators by new propositional variables. These new variables are axiomatized by declaring them equivalent with the replaced subformula. With this trick, for example all modal formulae can be put into a form with modal degree one, what greatly simplifies the calculus. The method is formalized and a completeness proof is given. Moreover, it is seen as a general method for transforming a cut-free Gentzen-type propositional system into a resolution-type system preserving the structure of derivations. This is a direct extension of Maslov’s method for classical predicate logic. An implementation of the method is mentioned.

03B35 Mechanization of proofs and logical operations
03F05 Cut-elimination and normal-form theorems
03B05 Classical propositional logic
03B20 Subsystems of classical logic (including intuitionistic logic)
03B45 Modal logic (including the logic of norms)
PDF BibTeX Cite