The Kreisel length-of-proof problem

DOI10.1007/BF01531022zbMath0865.03044MaRDI QIDQ1353977

William M. Farmer

Publication date: 13 May 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

first-order systemunificationPeano arithmeticKreisel length-of-proof propertyParikh system

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Related Items

The undecidability of proof search when equality is a logical connective, A unification algorithm for second-order monadic terms, A unification-theoretic method for investigating the \(k\)-provability problem, \(k\)-provability in \(\mathrm{PA}\)

Cites Work

• 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
• Unification theory
• The undecidability of the second-order unification problem
• On the length of proofs in formal systems
• A theorem on the formalized arithmetic with function symbols ' and +
• A note on a formalized arithmetic with function symbols ' and +
• A unification-theoretic method for investigating the \(k\)-provability problem
• Taking out LK parts from a proof in Peano arithmetic
• Unification: a multidisciplinary survey
• Sets of theorems with short proofs
• One hundred and two problems in mathematical logic
• A simplified formalization of predicate logic with identity
• Some Results on the Length of Proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item