On the form of witness terms

DOI10.1007/S00153-010-0186-7zbMATH Open1205.03064OpenAlexW2105870119MaRDI QIDQ982183FDOQ982183

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)

Cites Work

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

Cited In (1)

• On the compressibility of finite languages and formal proofs

Uses Software

• CERES

   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 👍 👎

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)