The Complexity of Propositional Proofs
From MaRDI portal
Publication:4873893
DOI10.2307/421131zbMath0845.03025OpenAlexW1940223960MaRDI QIDQ4873893
Publication date: 9 September 1996
Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/39dae84f0899bf3ddde5946e3678af9015a0b960
surveytableauxlower boundscomplexity of proofsresolutionsGentzen systemsFrege systemstruth tablesclassical propositional calculus\(k\)-valuation
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical propositional logic (03B05) Complexity of proofs (03F20)
Related Items
Interpolation systems for ground proofs in automated deduction: a survey, The proof complexity of linear algebra, Propositional SAT Solving, On an optimal quantified propositional proof system nal proof system and a complete language for NP ∩ co-NP for NP ∩ co-NP, An answer to an open problem of Urquhart, A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints, Regular and General Resolution: An Improved Separation, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Optimal proof systems imply complete sets for promise classes, Non-transitive correspondence analysis, Unit read-once refutations for systems of difference constraints, Resolution and binary decision diagrams cannot simulate each other polynomially, Homomorphisms of conjunctive normal forms., Limitations of Restricted Branching in Clause Learning, Simulating strong practical proof systems with extended resolution, Resolution remains hard under equivalence, On a generalization of extended resolution, The symmetry rule in propositional logic, On the elimination of quantifier-free cuts, An Introduction to Lower Bounds on Resolution Proof Systems, Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints, Finding the Hardest Formulas for Resolution, Finding read-once resolution refutations in systems of 2CNF clauses, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution, Partially definable forcing and bounded arithmetic, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity, The complexity of the Hajós calculus for planar graphs, Simulation of Natural Deduction and Gentzen Sequent Calculus, On the correspondence between arithmetic theories and propositional proof systems – a survey, NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability, Analyzing unit read-once refutations in difference constraint systems, Non-clausal redundancy properties, Computational properties of argument systems satisfying graph-theoretic constraints, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Complexity of translations from resolution to sequent calculus, The proof complexity of analytic and clausal tableaux, EXPtime tableaux for ALC, On Exponential Lower Bounds for Partially Ordered Resolution, Proofs and Certificates for Max-SAT, A Logical Autobiography, Reflections on Proof Complexity and Counting Principles, Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals, MaxSAT Resolution and Subcube Sums, Two party immediate response disputes: Properties and efficiency, A proof builder for Max-SAT
