Proving unsatisfiability of CNFs locally

DOI10.1023/A:1015803927637zbMath0995.03011OpenAlexW1540003216MaRDI QIDQ1610678

Eugene Goldberg

Publication date: 20 August 2002

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1015803927637

zbMATH Keywords

satisfiabilityconjunctive normal form

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

Boundary Points and Resolution

Cites Work

• Unnamed Item
• The intractability of resolution
• Hard examples for resolution
• Short proofs are narrow—resolution made simple
• GRASP: a search algorithm for propositional satisfiability
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving

This page was built for publication: Proving unsatisfiability of CNFs locally