Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
DOI10.1016/J.APAL.2007.10.010zbMATH Open1153.03040OpenAlexW2030319866MaRDI QIDQ930260FDOQ930260
Publication date: 23 June 2008
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.2007.10.010
proof complexitygeneralization of proofsmodification of Kreisel's conjecturemonadic languagepartial proof datauniform derivability of a proof schema
Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07) First-order arithmetic and fragments (03F30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
- One hundred and two problems in mathematical logic
- Proof theory
- Title not available (Why is that?)
- The number of proof lines and the size of proofs in first order logic
- Some Results on the Length of Proofs
- Foundations of mathematics for the working mathematician
- Title not available (Why is that?)
- Title not available (Why is that?)
- On GΓΆdel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
- On the number of steps in proofs
- The undecidability of the second-order unification problem
- Title not available (Why is that?)
- The undecidability of \(k\)-provability
- Sets of theorems with short proofs
- A unification algorithm for second-order monadic terms
- Title not available (Why is that?)
- A theorem on generalizations of proofs
- Title not available (Why is that?)
- Some applications of formalized consistency proofs
- Title not available (Why is that?)
- Arithmetic on curves
- Title not available (Why is that?)
- Title not available (Why is that?)
- Recursive Functions of One Variable
Cited In (7)
- Title not available (Why is that?)
- Note on the Benefit of Proof Representations by Name
- Title not available (Why is that?)
- A Proof-theoretic Treatment of Assignments
- Herbrand's theorem and term induction
- Title not available (Why is that?)
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
Recommendations
- Title not available (Why is that?) π π
- Theories very close to PA where Kreisel's Conjecture is false π π
- Kreisel's Conjecture with minimality principle π π
- The lengths of proofs: Kreisel's conjecture and GΓΆdel's speed-up theorem π π
- Title not available (Why is that?) π π
- The undecidability of \(k\)-provability π π
- Title not available (Why is that?) π π
- Bounded Induction and Satisfaction Classes π π
- Simple axioms that are obviously true in \(\mathbb{N}\) π π
- The Kreisel length-of-proof problem π π
This page was built for publication: Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q930260)