Describing proofs by short tautologies

DOI10.1016/j.apal.2008.10.010zbMath1172.03027OpenAlexW1966337849MaRDI QIDQ1023053

Stefan Hetzl

Publication date: 10 June 2009

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2008.10.010

zbMATH Keywords

proof theorycut-eliminationHerbrand's theorem

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items

Algorithmic introduction of quantified cuts ⋮ On the elimination of quantifier-free cuts ⋮ On the form of witness terms

Uses Software

• CERES

Cites Work

• Unnamed Item
• Unnamed Item
• Interpolants, cut elimination and flow graphs for the propositional calculus
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Proof theory. 2nd ed
• Cut normal forms and proof complexity
• Untersuchungen über das logische Schliessen. I
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Proof Transformations and Structural Invariance
• Proof Transformation by CERES
• Cut-elimination and redundancy-elimination by resolution