Bounds for proof-search and speed-up in the predicate calculus
From MaRDI portal
Publication:4198749
DOI10.1016/0003-4843(78)90011-6zbMath0411.03047OpenAlexW2056365917MaRDI QIDQ4198749
Publication date: 1978
Published in: Annals of Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0003-4843(78)90011-6
predicate calculusproof theoryspeed-upcut-eleminationlength of derivationslengths of proofsbounds for proof searchnormal-form theorem
Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)
Related Items
Upper bound on the lengthening of proofs by cut elimination, Structure of proofs and the complexity of cut elimination, The cost of a cycle is a square, A Subatomic Proof System for Decision Trees, A proper hierarchy of propositional sequent calculi, The number of proof lines and the size of proofs in first order logic, Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus, Lower bounds to the size of constant-depth propositional proofs, On the number of steps in proofs, On the Power of Substitution in the Calculus of Structures, Speed-Up by Theories with Infinite Models, On feasible numbers, Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic, Taking out LK parts from a proof in Peano arithmetic, Automatic theorem proving. II, Lifting lower bounds for tree-like proofs, The Story of $$\gamma $$ γ, On sets, types, fixed points, and checkerboards, Cut formulas in propositional logic, The Functional Interpretation of Direct Computations, Asymptotic cyclic expansion and bridge groups of formal proofs, Extension without cut, Cycling in proofs and feasibility, The complexity of Gentzen systems for propositional logic, A unification-theoretic method for investigating the \(k\)-provability problem, Meeting of the Association for Symbolic Logic, New York, 1979, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, Turning cycles into spirals, Fragments of bounded arithmetic and the lengths of proofs, Natural Deduction for Equality: The Missing Entity, Streams and strings in formal proofs., Cuts, consistency statements and interpretations
