Details:
Title  Using the Groebner basis algorithm to find proofs of unsatisfiability  Author(s)  Matthew Clegg, Jeffery Edmonds, Russell Impagliazzo  Type  Article in Conference Proceedings  Abstract  A propositional proof system can be viewed as a nondeterministic
algorithm for the (coNP complete) unsatisfiability problem.
Many such proof systems, such as resolution, are also used as
the basis for heuristics which deterministically search for short
proofs in the system.
We discuss a propositional proof system based on algebraic reasoning,
which we call the Groebner proof system because of a tight
connection to the Groebner basis algorithm. For an appropriate
measure of proof size, we show that (a degreelimited implementation
of) the Groebner basis algorithm finds a Groebner proof of a
tautology in time polynomial in the size of the smallest such proof,
In other words, unlike most proof systems, the nondeterministic
algorithm can be converted to a deterministic one without loss in
power.
We then compare the power of the Groebner proof system to
more studied systems. We show that the Groebner system polynomially
simulates Horn clause resolution, quasipolynomially simulates
tree... 
URL 
http://doi.acm.org/10.1145/237814.237860 
Language  English  Pages  174183  Year  1996  Edition  0  Translation 
No  Refereed 
No 
