کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6875274 | 1441593 | 2018 | 27 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Exploration of language specifications by compilation to first-order logic
ترجمه فارسی عنوان
اکتشاف خصوصیات زبان با تدوین به منطق مرتبه اول
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
سیستم های نوع مشخصات رسمی، زبانهای اعلام شده اولین قضیه ثابت کرد، زبانهای خاص دامنه
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
In this paper, we first present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As benchmarks, we developed language specifications for typed SQL and for a Questionnaire Language (QL), with 50 exploration goals each. Our study empirically confirms that the choice of a compilation strategy greatly influences prover performance in general and shows which strategies are advantageous for prover performance. Second, we extend our empirical study with 4 domain-specific strategies for axiom selection and find that axiom selection does not influence prover performance in our benchmark specifications.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 155, 1 April 2018, Pages 146-172
Journal: Science of Computer Programming - Volume 155, 1 April 2018, Pages 146-172
نویسندگان
Sylvia Grewe, Sebastian Erdweg, André Pacak, Michael Raulf, Mira Mezini,