scientific article; zbMATH DE number 1215500

zbMath0920.03056MaRDI QIDQ4215637

Pavel Pudlák

Publication date: 8 December 1998

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

lower boundsunificationbounded arithmeticproof systemsFrege systemsinterpolantspigeonhole principlesKreisel's conjecturelengths of proofscutting plane proofsarithmetic theoriesGroebner proof systemsequence form of proofsspeed-up theoremstree form of proofs

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical first-order logic (03B10) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (43)

Nondeterministic functions and the existence of optimal proof systems ⋮ Proof complexity and textual cohesion ⋮ The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem ⋮ Randomized feasible interpolation and monotone circuits with a local oracle ⋮ Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete ⋮ Short proofs for slow consistency ⋮ A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝 Frege systems] ⋮ Logical omniscience as infeasibility ⋮ On the generation of quantified lemmas ⋮ Rasiowa-Sikorski deduction systems with the rule of cut: a case study ⋮ TRUTH AND FEASIBLE REDUCIBILITY ⋮ HOW STRONG IS RAMSEY’S THEOREM IF INFINITY CAN BE WEAK? ⋮ The small‐is‐very‐small principle ⋮ A note on SAT algorithms and proof complexity ⋮ On the compressibility of finite languages and formal proofs ⋮ Non-elementary speed-ups in logic calculi ⋮ Truth definition for $\Delta _ 0$ formulas and PSPACE computations ⋮ The Story of $$\gamma $$ γ ⋮ Physics and proof theory ⋮ Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution ⋮ Partially definable forcing and bounded arithmetic ⋮ Proof systems that take advice ⋮ Herbrand's theorem and term induction ⋮ A complexity analysis of functional interpretations ⋮ The complexity of the Hajós calculus for planar graphs ⋮ Paraconsistent informational logic ⋮ On the form of witness terms ⋮ Mean-payoff games and propositional proofs ⋮ Understanding cutting planes for QBFs ⋮ The quantifier complexity of polynomial-size iterated definitions in first-order logic ⋮ A PARAMETRIC, RESOURCE-BOUNDED GENERALIZATION OF LÖB’S THEOREM, AND A ROBUST COOPERATION CRITERION FOR OPEN-SOURCE GAME THEORY ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ Interpreting Weak König’s Lemma using the Arithmetized Completeness Theorem ⋮ Proof Complexity of Non-classical Logics ⋮ Describing proofs by short tautologies ⋮ A Measure of Logical Inference and Its Game Theoretical Applications ⋮ Truth, disjunction, and induction ⋮ Some applications of propositional logic to cellular automata ⋮ Compressibility of Finite Languages by Grammars ⋮ The complexity of the disjunction and existential properties in intuitionistic logic ⋮ A feasible interpolation for random resolution ⋮ Saturated models of universal theories ⋮ Two party immediate response disputes: Properties and efficiency

This page was built for publication: