scientific article; zbMATH DE number 481931
From MaRDI portal
Publication:4274311
zbMath0808.03040MaRDI QIDQ4274311
Publication date: 14 December 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
arithmeticcomplexity of proofsHilbert-type calculibalanced binary search treesbound for cut-elimination in predicate logicterm equations with substitutions
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)
Related Items (13)
Proof complexity and textual cohesion ⋮ Essential structure of proofs as a measure of complexity ⋮ Checking Proofs ⋮ Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic ⋮ Negation-free and contradiction-free proof of the Steiner-Lehmus theorem ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ Cut rule for the resolution method ⋮ A complexity analysis of functional interpretations ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ \(k\)-provability in \(\mathrm{PA}\) ⋮ Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) ⋮ Invertible infinitary calculus without loop rules for restricted FTL
This page was built for publication:
