Theorem proving with the real numbers

Meer over het boek

This book explores the application of real numbers in theorem proving, addressing the limitations of typical theorem provers that primarily support discrete datatypes like natural numbers. The inclusion of real numbers significantly enhances the scope of applications, including the verification of floating-point hardware and hybrid systems, and facilitates the formalization of various branches of classical mathematics, which is crucial for increasing the rigor in computer algebra systems. The research is conducted using a version of the HOL theorem prover, detailing a rigorous definitional construction of real numbers through an updated Cantor's method and the formalization of a substantial portion of real analysis. It also introduces an advanced decision procedure for the 'Tarski subset' of real algebra, alongside practical tools for automating explicit calculations and linear arithmetic reasoning. The book further examines two key application areas: the integration of theorem provers with computer algebra systems for enhanced rigor and convenience, and the verification of floating-point hardware, including a discussion on correctness specifications and two case studies, one of which involves a transcendental function.