Gentzen-type systems, resolution and tableaux
type: Item
instance of: scholarly article
title: Gentzen-type systems, resolution and tableaux
zbMATH Open document ID: 0788.03013
DOI: 10.1007/BF00881838
author: Arnon Avron
published in: Journal of Automated Reasoning
publication date: 1994-06-05T00:00:00Z
review text: \textit{S. Yu. Maslov} introduced [Zap. Nauchn. Semin. Leningrad. Otd. Mat. Inst. Steklova 16, 137-146 (1969; Zbl 0199.315); English transl. in: J. Siekmann and G. Wrightson (eds.), Automation of reasoning. 2 (1983; Zbl 0567.03002)] a general method of transforming Gentzen-type derivations into resolution derivations which can be extended to a number of nonclassical systems [the reviewer, Lect. Notes Comput. Sci. 417, 198-231 (1990; Zbl 0739.03011)]. The author (who does not mention previous work in this direction) introduces another method for classical logic. It is based on the observation originating (in some form) with Gentzen: derivation from axioms (given as sequents) can be normalized to use cuts only over subformulas of the members of these sequents. If assumptions are clauses of the form \(\Rightarrow L_ 1, \dots, L_ n\) where \(L_ i\) are literals, all cuts are resolutions. The author hopes that the possibility to combine resolution and Gentzen-type rules may be useful in automated deduction. It would be interesting to see examples which can be done in this way, but cannot be done by resolution in reasonable time.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 484779
zbMATH Keywords: transforming Gentzen-type derivations into resolution derivations
zbMATH Keywords: classical logic
zbMATH Keywords: cuts
zbMATH Keywords: automated deduction
reviewed by: G. E. Mints
MaRDI profile type: Publication
cites work: Simple consequence relations
cites work: Q3954845
cites work: Q4132480
cites work: Q3327746
cites work: Q5679729
cites work: Q3996619
cites work: Q3743300
cites work: Q3994895
cites work: Q3773876
cites work: Q3862380
cites work: Q4139711
cites work: Q3783630
cites work: Q3864488
cites work: Q5560258
full work available at URL: https://doi.org/10.1007/bf00881838
OpenAlex ID: W2007013614
description: scientific article; zbMATH DE number 484779