کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
389318 661129 2016 17 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
ترجمه فارسی عنوان
قضیه اتوماتیک برای منطقهای چند متغیره با حل معادلات رضایت بخش ارائه می شود
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر هوش مصنوعی
چکیده انگلیسی

There is a relatively large number of papers dealing with complexity and proof theory issues of multiple-valued logics. Nevertheless, little attention has been paid so far to the development of efficient and robust solvers for such logics. In this paper we investigate how the technology of Satisfiability Modulo Theories (SMT) can be effectively used to build efficient automated theorem provers for relevant finitely-valued and infinitely-valued logics, taking the logics of Łukasiewicz, Gödel and Product as case studies. Besides, we report on an experimental investigation that evaluates the performance of SMT technology when solving multiple-valued logic problems, and compares the finitely-valued solvers for Łukasiewicz and Gödel logics with their infinitely-valued solvers from a computational point of view. We also compare the performance of SMT technology and MIP technology when testing the satisfiability on a genuine family of multiple-valued clausal forms.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Fuzzy Sets and Systems - Volume 292, 1 June 2016, Pages 32–48
نویسندگان
, , , ,