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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor
• Keywords: Automated Reasoning, CADE 2007, Order Connection Tableau, Order Theorem, Propositional Satisfiability Problems