Gentzen-type systems, resolution and tableaux (Q1311413)

\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.