کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4663059 | 1345224 | 2009 | 23 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Integrating external deduction tools with ACL2
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Integrating external deduction tools with ACL2 Integrating external deduction tools with ACL2](/preview/png/4663059.png)
چکیده انگلیسی
We present an interface connecting the ACL2 theorem prover with external deduction tools. The ACL2 logic contains several mechanisms for proof structuring, which are important to the construction of industrial-scale proofs. The complexity induced by these mechanisms makes the design of the interface challenging. We discuss some of the challenges, and develop a precise specification of the requirements on the external tools for a sound connection with ACL2. We also develop constructs within ACL2 to enable the developers of external tools to satisfy our specifications. The interface is available with the ACL2 theorem prover starting from Version 3.2, and we describe several applications of the interface.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 7, Issue 1, March 2009, Pages 3-25
Journal: Journal of Applied Logic - Volume 7, Issue 1, March 2009, Pages 3-25
نویسندگان
Matt Kaufmann, J Strother Moore J Strother Moore, Sandip Ray, Erik Reeber,