Regular and General Resolution: An Improved Separation

DOI10.1007/978-3-540-79719-7_26MaRDI QIDQ3502715zbMATH OpenOpenAlexFDO

Authors Alasdair Urquhart

Publication date 27 May 2008

Published in Theory and Applications of Satisfiability Testing – SAT 2008 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-79719-7_26

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• A near-optimal separation of regular and general resolution
• Width and size of regular resolution proofs
• Regular Resolution Versus Unrestricted Resolution
• The intractability of resolution
• On the relative complexity of resolution refinements and cutting planes proof systems

Cites work

• A DNF without Regular Shortest Consensus Path
• A machine program for theorem-proving
• scientific article; zbMATH DE number 5899257 (Why is no real title available?)
• scientific article; zbMATH DE number 1246230 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• Near optimal seperation of tree-like and general resolution
• Optimality of size-width tradeoffs for resolution
• Regular Resolution Versus Unrestricted Resolution
• Short proofs for tricky formulas
• Short resolution proofs for a sequence of tricky formulas
• Size space tradeoffs for resolution
• Space bounds for a game on graphs
• Tail bounds for occupancy and the satisfiability threshold conjecture
• The Complexity of Propositional Proofs

Cited in

(8)

• Strong ETH and resolution via games and the multiplicity of strategies
• An improved separation of regular resolution from pool resolution and clause learning
• A near-optimal separation of regular and general resolution
• Improved separations of regular resolution from clause learning proof systems
• The complexity of resolution refinements
• Strong ETH holds for regular resolution
• The depth of resolution proofs
• Regular resolution effectively simulates resolution

This page was built for publication: Regular and General Resolution: An Improved Separation

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