کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10325753 | 676800 | 2005 | 24 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Dealing with algebraic expressions over a field in Coq using Maple
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
We describe an interface between the Coq proof assistant and the Maple symbolic computation system, which mainly consists in importing, in Coq, Maple computations regarding algebraic expressions over fields. These can either be pure computations, which do not require any validation, or computations used during proofs, which must be proved (to be correct) within Coq. These correctness proofs are completed automatically thanks to the tactic Field, which deals with equalities over fields. This tactic, which may generate side conditions (regarding the denominators) that must be proved by the user, has been implemented in a reflexive way, which ensures both efficiency and certification. The implementation of this interface is quite light and can be very easily extended to get other Maple functions (in addition to the four functions we have imported and used in the examples given here).
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 569-592
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 569-592
نویسندگان
David Delahaye, Micaela Mayero,