On the form of witness terms

DOI10.1007/s00153-010-0186-7zbMath1205.03064OpenAlexW2105870119MaRDI QIDQ982183

Stefan Hetzl

Publication date: 6 July 2010

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-010-0186-7

zbMATH Keywords

Peano arithmeticcut-eliminationHerbrand's theorem

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Structure of proofs (03F07)

Related Items

On the compressibility of finite languages and formal proofs

Uses Software

• CERES

Cites Work

• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Describing proofs by short tautologies
• Proof theory. 2nd ed
• A compact representation of proofs
• Cut elimination and automatic proof procedures
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• General varieties of tree languages
• Turning cycles into spirals
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• The role of quantifier alternations in cut elimination
• Exploring the Computational Content of the Infinite Pigeonhole Principle
• The duality of computation
• On the non-confluence of cut-elimination
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• The correspondence between cut-elimination and normalization
• Lower Bounds on Herbrand's Theorem
• A new deconstructive logic: linear logic
• Cycling in proofs and feasibility
• Computer Science Logic
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Logic for Programming, Artificial Intelligence, and Reasoning
• The consistency of arithmetics
• Cut-elimination and redundancy-elimination by resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item