Describing proofs by short tautologies
type: Item
instance of: scholarly article
title: Describing proofs by short tautologies
zbMATH Open document ID: 1172.03027
author: Stefan Hetzl
published in: Annals of Pure and Applied Logic
publication date: 2009-06-10T00:00:00Z
review text: It is well-known that the size of Herbrand disjunction is super-exponential in the size of a proof (with cut or modus ponens). The author provides an elegant construction of a short propositional tautology similar to Herbrand disjunction and completely encoding a given proof. Assuming that a proved formula \(F\) as well as every cut formula in the proof is prenex, take all quantifier-free instances \(F_1,\ldots,F_k\) of \(F\) in the given proof, all quantifier-free instances \(C_1,\ldots,C_l\) of antecedent cut formulas and all quantifier-free instances \(D_1,\ldots,D_m\) of succedent cut formulas. The implication \((\bigvee_{i\leq l}C_i\rightarrow \&_{j\leq m}D_j)\rightarrow F_1\vee\ldots\vee F_k\) is proved by a quantifier-free derivation which encodes the previous derivation of \(F\).
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 5563896
zbMATH Keywords: proof theory
zbMATH Keywords: Herbrand's theorem
zbMATH Keywords: cut-elimination
reviewed by: G. E. Mints
describes a project that uses: CERES
MaRDI profile type: Publication
full work available at URL: j.apal.2008.10.010
OpenAlex ID: W1966337849
cites work: CERES: An analysis of Fürstenberg's proof of the infinity of primes
cites work: Proof Transformation by CERES
cites work: Q4304753
cites work: Cut normal forms and proof complexity
cites work: Cut-elimination and redundancy-elimination by resolution
cites work: Interpolants, cut elimination and flow graphs for the propositional calculus
cites work: Untersuchungen über das logische Schliessen. I
cites work: Proof Transformations and Structural Invariance
cites work: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
cites work: Q4215637
cites work: Proof theory. 2nd ed
DOI: 10.1016/J.APAL.2008.10.010
description: scientific article; zbMATH DE number 5563896