Lower bounds for increasing complexity of derivations after cut elimination

DOI10.1007/BF01629444zbMath0492.03023OpenAlexW1990529320MaRDI QIDQ1167721

V. P. Orevkov

Publication date: 1982

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01629444

zbMATH Keywords

lower bounds for proof length

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items

The number of axioms, Sharpened lower bounds for cut elimination, Andrews Skolemization may shorten resolution proofs non-elementarily, Unifying the model theory of first-order and second-order arithmetic via \(\mathrm{WKL}_0^\ast\), The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics, Herbrand complexity and the epsilon calculus with equality, UNSOUND INFERENCES MAKE PROOFS SHORTER, Translation of resolution proofs into short first-order proofs without choice axioms, Asymptotic cyclic expansion and bridge groups of formal proofs, Cycling in proofs and feasibility, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Complexity of translations from resolution to sequent calculus, Turning cycles into spirals, Cut normal forms and proof complexity, The complexity of the disjunction and existential properties in intuitionistic logic, Streams and strings in formal proofs., The epsilon calculus and Herbrand complexity

Cites Work

• Untersuchungen über das logische Schliessen. I
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item