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

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

Cites work

scientific article; zbMATH DE number 3900185 (Why is no real title available?)
scientific article; zbMATH DE number 3923729 (Why is no real title available?)
scientific article; zbMATH DE number 4049638 (Why is no real title available?)
scientific article; zbMATH DE number 3415409 (Why is no real title available?)
Bounds for proof-search and speed-up in the predicate calculus
On the length of proofs in formal systems
Proof theory
Some Results on the Length of Proofs
Some results on speed-up
The undecidability of the second-order unification problem

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
Generalizing theorems in real closed fields
Regular expression order-sorted unification and matching
Herbrand complexity and the epsilon calculus with equality
The number of axioms
1994–1995 Winter Meeting of the Association for Symbolic Logic
Upper bound on the height of terms in proofs with bound-depth-restricted cuts
Herbrand's theorem and term induction
Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
A tableaux-based decision procedure for multi-parameter propositional schemata
Proof schemata in Hilbert-type axiomatic theories
Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
On the non-confluence of cut-elimination
\(k\)-provability in \(\mathrm{PA}\)
Essential structure of proofs as a measure of complexity
The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
Asymptotic cyclic expansion and bridge groups of formal proofs
The undecidability of proof search when equality is a logical connective
On the compressibility of finite languages and formal proofs
A unification-theoretic method for investigating the \(k\)-provability problem
Bounded arithmetic, proof complexity and two papers of Parikh
The Kreisel length-of-proof problem
Depth of proofs, depth of cut-formulas and complexity of cut formulas
Refinement of bounds of the height of terms in the most general unifier
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)