Theorem Proving with the Real Numbers

این کتاب در مورد استفاده از اعداد حقیقی در اثبات قضیه بحث می کند. به طور معمول، اثبات‌کننده‌های قضیه فقط از چند نوع داده «گسسته» مانند اعداد طبیعی پشتیبانی می‌کنند. با این حال، در دسترس بودن اعداد واقعی بسیاری از زمینه‌های کاربردی جالب و مهم را باز می‌کند، مانند تأیید سخت‌افزار نقطه شناور و سیستم‌های ترکیبی. همچنین به رسمیت بخشیدن به بسیاری از شاخه‌های ریاضیات کلاسیک اجازه می‌دهد که به ویژه برای تلاش‌ها برای تزریق دقت بیشتر به سیستم‌های جبر رایانه‌ای مرتبط است. کار ما در نسخه ای از اثبات قضیه HOL انجام شده است. ما ساختار تعریف دقیق اعداد واقعی را با استفاده از نسخه جدیدی از روش کانتور و رسمی کردن بخش قابل توجهی از تحلیل واقعی توصیف می‌کنیم. ما همچنین یک روش تصمیم گیری مشتق شده پیشرفته را برای «زیرمجموعه تارسکی» جبر واقعی و همچنین برخی از ابزارهای ساده تر اما عملا مفید برای خودکار کردن محاسبات صریح و استدلال خطی معمولی توصیف می کنیم. در نهایت، دو حوزه کاربردی جالب را با جزئیات بیشتر در نظر می گیریم. ما در مورد مطلوبیت ترکیب سختی اثبات‌کننده‌های قضیه با قدرت و راحتی سیستم‌های جبر رایانه‌ای بحث می‌کنیم و روشی را که در عمل برای رسیدن به این هدف استفاده کرده‌ایم توضیح می‌دهیم. سپس به بررسی سخت افزار ممیز شناور می رویم. پس از بحث دقیق در مورد مشخصات صحت احتمالی، ما دو مطالعه موردی را گزارش می‌کنیم که یکی شامل یک تابع استعلایی است.

This book discusses the use of the real numbers in theorem proving. Typ­ ically, theorem provers only support a few 'discrete' datatypes such as the natural numbers. However the availability of the real numbers opens up many interesting and important application areas, such as the verification of float­ ing point hardware and hybrid systems. It also allows the formalization of many more branches of classical mathematics, which is particularly relevant for attempts to inject more rigour into computer algebra systems. Our work is conducted in a version of the HOL theorem prover. We de­ scribe the rigorous definitional construction of the real numbers, using a new version of Cantor's method, and the formalization of a significant portion of real analysis. We also describe an advanced derived decision procedure for the 'Tarski subset' of real algebra as well as some more modest but practically useful tools for automating explicit calculations and routine linear arithmetic reasoning. Finally, we consider in more detail two interesting application areas. We discuss the desirability of combining the rigour of theorem provers with the power and convenience of computer algebra systems, and explain a method we have used in practice to achieve this. We then move on to the verification of floating point hardware. After a careful discussion of possible correctness specifications, we report on two case studies, one involving a transcendental function.