کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
439363 690535 2006 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Strategies for combining decision procedures
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Strategies for combining decision procedures
چکیده انگلیسی

Implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. In this paper we describe an inference system that has the classical Nelson–Oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and Shostak's streamlined generation of new equalities for theories with solvers. The transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. In particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic Nelson–Oppen to the very highly optimized one recently given by Shankar and Rueß. Presenting the basic system at a high level of generality and non-determinism allows transparent correctness proofs that can be extended in a modular fashion when new features are introduced in the system.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 354, Issue 2, 28 March 2006, Pages 187-210