Using the Groebner basis algorithm to find proofs of unsatisfiability 论文

摘要

proof system can be viewed as a non-deterministic algorithm for the (co-NP complete) unsatisfiabilit y problem. Many such proof systems, such as resolution, are rdso used as the basis for heuristics which deterministicrdly search for short proofs in the system.