Theorem Proving with the Real Numbers

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...