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.

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.

Reviewer: H.J.Ohlbach (Saarbrücken)

##### MSC:

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) |