Gentzen systems, resolution, and literal trees
type: Item
instance of: scholarly article
title: Gentzen systems, resolution, and literal trees
zbMATH Open document ID: 0629.03038
author: Daniel J. Dougherty
published in: Notre Dame Journal of Formal Logic
publication date: 1986-01-01T00:00:00Z
review text: The paper deals with the length of proofs in various calculi for propositional logic, in particular Gentzen's sequential calculus and the resolution method. The method employed here uses transformations between proofs in the various systems. In particular, the author exhibits a sequential calculus \(G_ 1\) with cut whose proofs correspond exactly to the derivations in the resolution calculus. From the complexity results we mention that the system \(G_ 1\) is not a polynomially bounded proof system. Other results deal with extended resolution and cut elimination; of particular interest is that eliminating cuts never substantially shortens the proofs.
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F15
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 4023273
zbMATH Keywords: length of proofs
zbMATH Keywords: calculi for propositional logic
zbMATH Keywords: Gentzen's sequential calculus
zbMATH Keywords: resolution
zbMATH Keywords: extended resolution
zbMATH Keywords: cut elimination
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1093636762
OpenAlex ID: W2031157676
DOI: 10.1305/NDJFL/1093636762
description: scientific article; zbMATH DE number 4023273