On the form of witness terms

DOI10.1007/S00153-010-0186-7MaRDI QIDQ982183zbMATH OpenOpenAlexFDO

Authors 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

Herbrand's theoremPeano arithmeticcut-elimination

Mathematics Subject Classification ID

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

Recommendations

• On the non-confluence of cut-elimination
• Cut Elimination In Situ
• Cut-elimination and proof schemata
• Herbrand-confluence
• Proof Search Tree and Cut Elimination

Cites work

• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 3668590 (Why is no real title available?)
• scientific article; zbMATH DE number 3552620 (Why is no real title available?)
• scientific article; zbMATH DE number 1215493 (Why is no real title available?)
• scientific article; zbMATH DE number 1215500 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3327279 (Why is no real title available?)
• A compact representation of proofs
• A new deconstructive logic: linear logic
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Computer Science Logic
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Cut elimination and automatic proof procedures
• Cut-elimination and redundancy-elimination by resolution
• Cycling in proofs and feasibility
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Describing proofs by short tautologies
• Exploring the computational content of the infinite pigeonhole principle
• General varieties of tree languages
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• Logic for Programming, Artificial Intelligence, and Reasoning
• Lower Bounds on Herbrand's Theorem
• On the non-confluence of cut-elimination
• Proof theory. 2nd ed
• Strong normalisation of cut-elimination in classical logic
• The consistency of arithmetics
• The correspondence between cut-elimination and normalization
• The duality of computation
• The role of quantifier alternations in cut elimination
• Turning cycles into spirals
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(2)

• On the non-confluence of cut-elimination
• On the compressibility of finite languages and formal proofs

Describes a project that uses

Uses Software

• CERES

This page was built for publication: On the form of witness terms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q982183)