Sciweavers

Share
CADE
2007
Springer

Encoding First Order Proofs in SAT

12 years 7 days ago
Encoding First Order Proofs in SAT
We present a method for proving rigid first order theorems by encoding them as propositional satisfiability problems. We encode the existence of a first order connection tableau and the satisfiability of unification constraints. Then the first order theorem is rigidly unsatisfiable if and only if the encoding is propositionally satisfiable. We have implemented this method in our theorem prover CHEWTPTP, and present experimental results. This method can be useful for general first order problems, by continually adding more instances of each clause.
Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin,
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor
Comments (0)
books