A unification-theoretic method for investigating the \(k\)-provability problem
From MaRDI portal
Publication:1814133
DOI10.1016/0168-0072(91)90015-EzbMath0735.03001MaRDI QIDQ1814133
Publication date: 25 June 1992
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Peano arithmeticaxiomatic theoryParikh systemfirst-order axiomatic systemsk-provability problemsubproblems of the unification problem
Decidability of theories and sets of sentences (03B25) First-order arithmetic and fragments (03F30) Complexity of proofs (03F20)
Related Items
The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, The Kreisel length-of-proof problem, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, The undecidability of \(k\)-provability, Interpolants, cut elimination and flow graphs for the propositional calculus, Higher-order unification revisited: Complete sets of transformations, \(k\)-provability in \(\mathrm{PA}\), Bounded arithmetic, proof complexity and two papers of Parikh, Simple second-order languages for which unification is undecidable
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Simple second-order languages for which unification is undecidable
- The number of proof lines and the size of proofs in first order logic
- A unification algorithm for second-order monadic terms
- On the number of steps in proofs
- Unification theory
- Set theory. An introduction to independence proofs
- The undecidability of the second-order unification problem
- The undecidability of \(k\)-provability
- The Kreisel length-of-proof problem
- Unification: a multidisciplinary survey
- Sets of theorems with short proofs
- Bounds for proof-search and speed-up in the predicate calculus
- Hilbert's Tenth Problem is Unsolvable
- A Machine-Oriented Logic Based on the Resolution Principle
- A simplified formalization of predicate logic with identity
- Abbreviating proofs by adding new axioms
- Some Results on the Length of Proofs
