By Jacques Fleuriot PhD, MEng (auth.)

Sir Isaac Newton's philosophi Naturalis Principia Mathematica'(the Principia) incorporates a prose-style mix of geometric and restrict reasoning that has frequently been seen as logically vague.

In **A mixture of Geometry Theorem Proving and Nonstandard****Analysis**, Jacques Fleuriot offers a formalization of Lemmas and Propositions from the Principia utilizing a mix of equipment from geometry and nonstandard research. The mechanization of the methods, which respects a lot of Newton's unique reasoning, is built in the theorem prover Isabelle. the applying of this framework to the mechanization of ordinary actual research utilizing nonstandard innovations is usually discussed.

**Read Online or Download A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton’s Principia PDF**

**Similar geometry books**

**Geometry of Conics (Mathematical World)**

The ebook is dedicated to the homes of conics (plane curves of moment measure) that may be formulated and proved utilizing basically uncomplicated geometry. beginning with the well known optical homes of conics, the authors movement to much less trivial effects, either classical and modern. specifically, the bankruptcy on projective homes of conics includes a certain research of the polar correspondence, pencils of conics, and the Poncelet theorem.

**Geometrie der Raumzeit: Eine mathematische Einführung in die Relativitätstheorie**

Die Relativit? tstheorie ist in ihren Kernaussagen nicht mehr umstritten, gilt aber noch immer als kompliziert und nur schwer verstehbar. Das liegt unter anderem an dem aufwendigen mathematischen Apparat, der schon zur Formulierung ihrer Ergebnisse und erst recht zum Nachvollziehen der Argumentation notwendig ist.

**The Foundations of Geometry and the Non-Euclidean Plane**

This publication is a textual content for junior, senior, or first-year graduate classes ordinarily titled Foundations of Geometry and/or Non Euclidean Geometry. the 1st 29 chapters are for a semester or yr direction at the foundations of geometry. the rest chap ters might then be used for both a standard direction or autonomous research classes.

- An introduction to nonlinear analysis
- Geometry and Differential Geometry: Proceedings of a Conference Held at the University of Haifa, Israel, March 18–23, 1979
- Classical Geometries in Modern Contexts: Geometry of Real Inner Product Spaces
- Geometry of Spatial Forms - Alalysis, Synthesis, etc [for CAD]

**Additional resources for A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton’s Principia**

**Sample text**

20] also propose a method based on the concept of full-angles that can be used to deal with classes of theorems that pose problems to the area method. A full-angle (u, v) is the angle from line u to line v measured anti-clockwise. We note that u and v are lines rather than rays; this has the major advantage of simplifying proofs by eliminating case-splits in certain cases. The full-angle is then used to express other familiar geometric properties and augment the reasoning capabilities of the geometry theory.

Since the law of reflection means that the angle of incidence is the same as the angle of reflection, the above definition follows. Given a point on an ellipse, we are also interested in finding the set of points that belong to the tangent at that point. We add the following definition to deal with this situation: e_tangent x h fa E == {po is_e_tangent (x -- p) h fa E} Definitions relating to the tangent to the circle are also made straightforwardly in Isabelle. l a -- b) c_tangent a x C == {po is_c_tangent (a -- p) x C} Various theorems can be proved about ellipses, circles, and their tangents.

Or})" "lhr _ Abs_hypreal(hyprel··{An::nat. lr})" constdefs hypreal_minus :: hypreal :::} hypreal "- p _ Abs_hypreal(UXERep_hypreal(P). hyprel··{An: :nat. - (X n)})" (* embedding for the reals *) hypreal_of_real :: real:::} hypreal "hypreal_oCreal r == Abs_hypreal(hyprel··{An: :nat. r})" hrinv .. hypreal :::} hypreal "hrinv P == Abs_hypreal (UXE Rep_hypreal (P) . hyprel··{An. if X n = Or then Or else rinv (X n)})" defs hypreal_add_def IIp + Q == Abs_hypreal (UXERep_hypreal (P) . UYERep_hypreal(Q).