کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9656880 | 686148 | 2005 | 20 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Canonization for disjoint unions of theories
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the disjoint union of the two theories? We prove this is possible whenever the original theories are convex. As an application, we prove that algorithms for solving equations in the two theories (solvers) can not be combined in a similar fashion. These results are relevant to the widely used Shostak's method for combining decision procedures for theories. They provide the first rigorous answers to the questions about the possibility of directly combining canonizers and solvers.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 199, Issues 1â2, 25 Mayâ15 June 2005, Pages 87-106
Journal: Information and Computation - Volume 199, Issues 1â2, 25 Mayâ15 June 2005, Pages 87-106
نویسندگان
Sava KrstiÄ, Sylvain Conchon,