Herbrand's theorem and term induction

DOI10.1007/s00153-005-0327-6zbMath1093.03032OpenAlexW2009766573MaRDI QIDQ2491080

Matthias Baaz, Georg Moser

Publication date: 26 May 2006

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

Full work available at URL: https://doi.org/10.1007/s00153-005-0327-6

zbMATH Keywords

Herbrand's theoremcut-free proof systemterm induction

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Complexity of proofs (03F20)

Uses Software

• NQTHM

Cites Work

• Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
• Proof theory. 2nd ed
• The number of proof lines and the size of proofs in first order logic
• Cut normal forms and proof complexity
• Untersuchungen über das logische Schliessen. I
• Generalizing theorems in real closed fields
• Some results on speed-up
• Sets of theorems with short proofs
• Some Results on the Length of Proofs
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Herbrand's theorem and term induction