The complexity of resolution refinements

DOI10.2178/JSL/1203350790MaRDI QIDQ5444704zbMATH OpenOpenAlexFDO

Authors Joshua Buresh-Oppenheim, Toniann Pitassi

Publication date 25 February 2008

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://projecteuclid.org/euclid.jsl/1203350790

zbMATH Keywords

complexityresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On the relative complexity of resolution refinements and cutting planes proof systems
• Davis-Putnam resolution versus unrestricted resolution
• Regular and General Resolution: An Improved Separation
• Near optimal seperation of tree-like and general resolution
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning

Cites work

• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Davis-Putnam resolution versus unrestricted resolution
• Linear resolution with selection function
• On the relative complexity of resolution refinements and cutting planes proof systems
• Regular Resolution Versus Unrestricted Resolution
• The Complexity of Propositional Proofs
• The intractability of resolution
• Unrestricted resolution versus N-resolution

Cited in

(21)

• Resolvability vs. almost resolvability
• An average case analysis of a resolution principle algorithm in mechanical theorem proving.
• Resolution of space curves complexity
• Resolution in solving graph problems
• On the relative complexity of resolution refinements and cutting planes proof systems
• Resolution theorem proving
• On the Relative Strength of Pebbling and Resolution
• scientific article; zbMATH DE number 5613975 (Why is no real title available?)
• Unified Characterisations of Resolution Hardness Measures
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• On linear resolution
• scientific article; zbMATH DE number 7250156 (Why is no real title available?)
• On the Capacity of the Precision-Resolution System
• DNA Computing
• Solving satisfiability problems with preferences
• The Complexity of Angular Resolution
• On the use of naturality in algorithmic resolution
• Regular resolution effectively simulates resolution
• From quantifier depth to quantifier number: separating structures with k variables
• Near-optimal lower bounds on quantifier depth and Weisfeiler-Leman refinement steps
• Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable

This page was built for publication: The complexity of resolution refinements

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5444704)