کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
401855 | 676727 | 2010 | 28 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A verified Common Lisp implementation of Buchberger’s algorithm in ACL2
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 45, Issue 1, January 2010, Pages 96-123
Journal: Journal of Symbolic Computation - Volume 45, Issue 1, January 2010, Pages 96-123