کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423665 685273 2008 14 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Encoding First Order Proofs in SMT
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Encoding First Order Proofs in SMT
چکیده انگلیسی

We present a method for encoding first order proofs in SMT. Our implementation, called ChewTPTP-SMT, transforms a set of first order clauses into a propositional encoding (modulo theories) of the existence of a rigid first order connection tableau and the satisfiability of unification constraints, which is then fed to Yices. For the unification constraints, terms are represented as recursive datatypes, and unification constraints are equations on terms. The finiteness of the tableau is encoded by linear real arithmetic inequalities.We compare our implementation with our previous implementation ChewTPTP-SAT, encoding rigid connection tableau in SAT, and show that for Horn clauses many fewer propositional clauses are generated by ChewTPTP-SMT, and ChewTPTP-SMT is much faster than ChewTPTP-SAT. This is not the case for our non-Horn clause encoding. We explain this, and we conjecture a rule of thumb on when to use theories in encoding a problem.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 198, Issue 2, 6 May 2008, Pages 71-84