Euclid

Deciding Statments in Euclidean Geometry

This is a proof of concept of an application of commutative algebra to deciding statements about Euclidean geometry. We translate possible hypotheses and conclusions to multivariate polynomials. From these we form an algebraic variety V. The conclusion then follows from the hypotheses if and only if it is contained in the ideal of the polynomial ring R[a,b,...] which vanishes on V. We test this by computing the reduced Groebner basis of a modified ideal. Consult [Cox et al, 2010] for further reference.

Examples

Tautologies:

$ cat test
parallel (AB,CD); decide parallel(AB,CD)
$ ./main test
Judgment: yes

$ cat test
parallel (AB,CD); decide parallel(AD,BC)
$ ./main test
Judgment: no

The parallelogram theorem:

$ cat test
parallel (AB,CD); parallel(AC, BD); colin (A,N,D); colin (B,N,C);
decide disteq(AN,ND)
$ ./main test
Judgment: yes

Removing the requirement that AND are collinear breaks the theorem:

$ cat test
parallel (AB,CD); parallel(AC, BD); colin (B,N,C);
decide disteq(AN,ND)
$ ./main test
Judgment: no

Supported Syntax

We support the following constructs:

• parallel (AB,CD) - AB is parallel to CD;
• perp (AB,CD) - AB is perpendicular to CD;
• colin (A,B,C) - A, B, C are collinear;
• disteq (AB,CD) - |AB| = |CD|;
• circle (C,A,AB) - C lies on the circle with center A and radius AB;
• midpoint (A,B,C) - A is the midpoint of BC;
• angleeq (ABC,DEF) - angle ABC equals angle DEF (both acute);
• bisects(BD,ABC) - BD bisects angle ABC.

Limitations

• Statements are decided over the complex plane C rather than the real plane. [Sturmfels 1989] gives examples of complicated statements which will hence fail here.
• We are unable to output a proof of any conclusions, only give a judgment as to whether they follow. One possible future direction is to create a reverse translation between polynomials and geometric statements and then convert each intermediate result of the basis algorithm back to the language of geometry.

Building

A Makefile has been provided, allowing you to build the project with only the default OCaml installation. OCaml 4.01 is required; this requirement may be relaxed by replacing the application operator (|>) with fun x g -> g x.

$ make

This will generate a native binary. You can generate OCaml bytecode instead by replacing ocamlopt with ocamlc in the Makefile.

License

This project is licensed under the MIT open source license.