The number of proof lines and the size of proofs in first order logic

DOI10.1007/BF01625836zbMath0644.03032WikidataQ106785191 ScholiaQ106785191MaRDI QIDQ1102280

Pavel Pudlák, Jan Krajíček

Publication date: 1988

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

zbMATH Keywords

complexityupper boundsGentzen's calculus LKnumber of proof linessize of a formulasize of a proofsize of a sequent

Mathematics Subject Classification ID

Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (32)

The number of axioms ⋮ Depth of proofs, depth of cut-formulas and complexity of cut formulas ⋮ The undecidability of proof search when equality is a logical connective ⋮ The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem ⋮ The Kreisel length-of-proof problem ⋮ Generalizing theorems in real closed fields ⋮ A theorem on generalizations of proofs ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ On the number of steps in proofs ⋮ Essential structure of proofs as a measure of complexity ⋮ 1994–1995 Winter Meeting of the Association for Symbolic Logic ⋮ Herbrand complexity and the epsilon calculus with equality ⋮ On the compressibility of finite languages and formal proofs ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ The undecidability of \(k\)-provability ⋮ Refinement of bounds of the height of terms in the most general unifier ⋮ Note on the Benefit of Proof Representations by Name ⋮ Interpolants, cut elimination and flow graphs for the propositional calculus ⋮ Cut-elimination: syntax and semantics ⋮ Herbrand's theorem and term induction ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ Proof schemata in Hilbert-type axiomatic theories ⋮ Regular expression order-sorted unification and matching ⋮ On the non-confluence of cut-elimination ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Kreisel's Conjecture with minimality principle ⋮ \(k\)-provability in \(\mathrm{PA}\) ⋮ Informational logic for automated reasoning ⋮ A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata ⋮ Controlling witnesses ⋮ Bounded arithmetic, proof complexity and two papers of Parikh ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of the second-order unification problem
• On the length of proofs in formal systems
• Some results on speed-up
• Bounds for proof-search and speed-up in the predicate calculus
• Some Results on the Length of Proofs
• Proof theory

This page was built for publication: The number of proof lines and the size of proofs in first order logic