The various chapters of this book have covered the development of a range of theories in the theorem prover Isabelle. The main unifying theme has been the use of infinitesimals as valuable tools that are once again respectable in mathematics. Infinitesimals have been around for over 2 000 years and generally had a bad press. Their use has at times been free and viewed as a blessing (throughout the eighteenth century, for example), and at others viewed as heresy and banned (from the nineteenth century until the middle of this century). What is undeniable is that they have been valued as intuitive tools at all times by generations of mathematicians who used them to solve problems and carry out proofs. Even those trying to get rid of them sometimes lapsed into infinitesimal reasoning. The great insight of Robinson, leading to the creation of NSA, has been praised over and over again. In a sense, his work vindicates the (sometimes blind) faith of influential mathematicians such as the Marquis de L’Hospital in the use of infinitesimals. The major achievement of Robinson and his followers was not only to rehabilitate the infinitesimal as a sound mathematical concept but also to bring along new types of numbers that added to the power of the nonstandard approach.


Number System Euclidean Geometry Differential Calculus Diagrammatic Reasoning Geometry Theorem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2001

Authors and Affiliations

  • Jacques Fleuriot
    • 1
  1. 1.Division of InformaticsUniversity of EdinburghEdinburghUK

Personalised recommendations