کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10325752 | 676800 | 2005 | 29 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Hidden verification for computational mathematics
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Hidden verification for computational mathematics Hidden verification for computational mathematics](/preview/png/10325752.png)
چکیده انگلیسی
We present hidden verification as a means to make the power of computational logic available to users of computer algebra systems while shielding them from its complexity. We have implemented in PVS a library of facts about elementary and transcendental functions, and automatic procedures to attempt proofs of continuity, convergence and differentiability for functions in this class. These are called directly from Maple by a simple pipe-lined interface. Hence we are able to support the analysis of differential equations in Maple by direct calls to PVS for: result refinement and verification, discharge of verification conditions, harnesses to ensure more reliable differential equation solvers, and verifiable look-up tables.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 539-567
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 539-567
نویسندگان
Hanne Gottliebsen, Tom Kelsey, Ursula Martin,