Propositional proof systems, the consistency of first order theories and the complexity of computations
From MaRDI portal
DOI10.2307/2274765zbMATH Open0696.03029OpenAlexW2171353564WikidataQ106785096 ScholiaQ106785096MaRDI QIDQ3472096FDOQ3472096
Authors: Jan Krajíček, Pavel Pudlák 
Publication date: 1989
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2274765
Recommendations
Classical propositional logic (03B05) Classical first-order logic (03B10) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Complexity of computation (including implicit computational complexity) (03D15) Turing machines and related notions (03D10)
Cites Work
Cited In (78)
- P-Optimal Proof Systems for Each NP-Set but no Complete Disjoint NP-Pairs Relative to an Oracle
- Automated Deduction – CADE-20
- Frege proof system and TNC°
- Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)
- On the Power of Substitution in the Calculus of Structures
- INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
- Some consequences of cryptographical conjectures for S 2 1 and EF
- A Tight Karp-Lipton Collapse Result in Bounded Arithmetic
- Title not available (Why is that?)
- Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- Frege proof system and TNC°
- Title not available (Why is that?)
- Further oracles separating conjectures about incompleteness in the finite domain
- Substitution and Propositional Proof Complexity
- An oracle separating conjectures about incompleteness in the finite domain
- On a generalization of extended resolution
- Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes
- European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988
- The Deduction Theorem for Strong Propositional Proof Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Functional interpretations of feasibly constructive arithmetic
- Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds
- Towards NP-P via proof complexity and search
- The Complexity of Propositional Proofs
- Nondeterministic functions and the existence of optimal proof systems
- ON THE PROOF COMPLEXITY OF THE NISAN–WIGDERSON GENERATOR BASED ON A HARD NP ∩ coNP FUNCTION
- Classes of representable disjoint \textsf{NP}-pairs
- Tuples of disjoint \(\mathsf{NP}\)-sets
- Combinatorics of first order structures and propositional proof systems
- Extension without cut
- On an optimal randomized acceptor for graph nonisomorphism
- A Parameterized Halting Problem
- On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography
- Propositional truth maintenance systems: Classification and complexity analysis
- Proof systems that take advice
- Total nondeterministic Turing machines and a p-optimal proof system for SAT
- The deduction theorem for strong propositional proof systems
- The symmetry rule in propositional logic
- Proof complexity of non-classical logics
- On reducibility and symmetry of disjoint NP pairs.
- Propositional consistency proofs
- On optimal inverters
- A note on SAT algorithms and proof complexity
- Optimal proof systems imply complete sets for promise classes
- Reduction of Hilbert-type proof systems to the if-then-else equational logic
- Propositional proof systems and fast consistency provers
- On an optimal propositional proof system and the structure of easy subsets of TAUT.
- Refutational theorem proving for hierarchic first-order theories
- Computer runtimes and the length of proofs. With an algorithmic probabilistic application to waiting times in automatic theorem proving
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- Some remarks on lengths of propositional proofs
- Title not available (Why is that?)
- Do there exist complete sets for promise classes?
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- Speedup for natural problems and noncomputability
- On the complexity of Gödel's proof predicate
- Tautologies from pseudo-random generators
- Hardness assumptions in the foundations of theoretical computer science
- Propositional proof complexity
- Title not available (Why is that?)
- Title not available (Why is that?)
- On deciding the truth of certain statements involving the notion of consistency
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- INCOMPLETENESS IN THE FINITE DOMAIN
- Optimal heuristic algorithms for the image of an injective function
- Implicit proofs
- THE INFORMATIONAL CONTENT OF CANONICAL DISJOINT NP-PAIRS
- The number of proof lines and the size of proofs in first order logic
- NEW RELATIONS AND SEPARATIONS OF CONJECTURES ABOUT INCOMPLETENESS IN THE FINITE DOMAIN
- Logical Closure Properties of Propositional Proof Systems
- ALOGTIME and a conjecture of S. A. Cook
- Nondeterministic Instance Complexity and Proof Systems with Advice
- Does Advice Help to Prove Propositional Tautologies?
- Consistency and optimality
- On an optimal quantified propositional proof system nal proof system and a complete language for NP ∩ co-NP for NP ∩ co-NP
- On first-order theorem proving using generalized odd-superpositions II
This page was built for publication: Propositional proof systems, the consistency of first order theories and the complexity of computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3472096)
