کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423326 685205 2006 12 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Tool Building Requirements for an API to First-Order Solvers
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Tool Building Requirements for an API to First-Order Solvers
چکیده انگلیسی

Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into expressive interactive frameworks for logical deduction, such as higher-order logic theorem provers. This paper states some pragmatic requirements for implementations of decision procedures that make them well-suited to integration into such frameworks. The aim is to open a dialogue with the designers of decision procedure software that will lead to greater and easier uptake of their implementations by verification users.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 144, Issue 2, 19 January 2006, Pages 15-26