کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10325754 | 676800 | 2005 | 23 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Automated conjecture making in number theory using HR, Otter and Maple
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Experience has shown that HR produces too many conjectures which can be easily proven from the definitions of the functions involved. Hence, we use the Otter theorem prover to discard any theorems which can be easily proven, leaving behind the more interesting ones which are empirically plausible but not easily provable. We describe the core functionality of HR which enables it to form a theory, and the additional functionality implemented in order for HR to work with Maple functions. We present two experiments where we have applied HR's theory formation in number theory. We discuss the modes of operation for the user and provide some of the results produced in this way. We hope to show that using HR, Otter and Maple in this fashion has much potential for the advancement of computer algebra systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 593-615
Journal: Journal of Symbolic Computation - Volume 39, Issue 5, May 2005, Pages 593-615
نویسندگان
Simon Colton,