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

DOI10.1007/BF01625836zbMATH Open0644.03032WikidataQ106785191 ScholiaQ106785191MaRDI QIDQ1102280FDOQ1102280

Authors: Jan Krajíček, Pavel Pudlák 

Publication date: 1988

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

Recommendations

• Quantified propositional logic and the number of lines of tree-like proofs
• On structuring proof search for first order linear logic
• On structuring proof search for first order linear logic
• The succinctness of first-order logic on linear orders
• Proofs as computations in linear logic
• scientific article; zbMATH DE number 1751350
• scientific article; zbMATH DE number 1292302
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• scientific article; zbMATH DE number 1070624
• On lengths of proofs in non-classical logics

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)

Cites Work

• Title not available (Why is that?)
• Proof theory
• Some Results on the Length of Proofs
• Bounds for proof-search and speed-up in the predicate calculus
• The undecidability of the second-order unification problem
• Some results on speed-up
• Title not available (Why is that?)
• On the length of proofs in formal systems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (34)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1102280)