• an instantiation scheme for satisfiability modulo theories

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 782
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     state-of-the-art theory solvers generally rely on an instantiation of the axioms of the theory, and depending on the solvers, this instantiation is more or less explicit. this paper introduces a generic instantiation scheme for solving smt problems, along with syntactic criteria to identify the classes of clauses for which it is complete. the instantiation scheme itself is simple to implement, and we have produced an implementation of the syntactic criteria that guarantee a given set of clauses can be safely instantiated. we used our implementation to test the completeness of our scheme for several theories of interest in the smt community, some of which are listed in the last section of this paper.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها