Example of Automated Theorem Proving
in Theorema

Automated Proof of Geometrical Theorems Using Gröbner Bases

The Butterfly Theorem

Textbook formulation:

A, B, C and D are four points on circle (O). E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD at F and BC at G. Show that (OverBar[FE]) = (OverBar[GE]).

Input to the system:

Proposition["Butterfly", any[O, A, B, C, D, EE, F, G], 
      point[O, A] ∧ 
pon[C, 
            circle[O, A]] ∧ 
pon[B, 
            circle[O, A]] ∧ 
pon[D, 
            circle[O, A]] ∧ 
inter[EE, line[A, C], 
            line[B, D]] ∧ inter[F, line[D, A], tline[EE, EE, O]] ∧ 
          inter[G, line[B, C], line[EE, F]]
 \[Implies] 
        distequal[EE, F, G, EE]]

Input to the system:

Simplify[Proposition["Butterfly"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Butterfly_g", 
      any[O, A, B, C, 
        D], {{ O, {100, 100}}, {A, {0, 100}}, {B, {55, 
            190}}, {C, {171, 170}}, {D, {60, 10}}}]

Input to the system:

Simplify[Proposition["Butterfly"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Butterfly_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Butterfly"], 
      by -> GeometryProver]

Inserted notebook generated automatically by the system

End of inserted notebook

Pappus' Theorem

Textbook formulation:

Let A,  B,  C and A1,  B1,  C1 be on two lines and P = A B1 ⋂ A1  B, Q = A  C1 ⋂ A1  C, S = B  C1 ⋂ B1  C. Then P, Q, and S are collinear.

Input to the system:

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
inter[
            Q, line[A, C1], line[A1, C]] ∧ 
inter[S, 
            line[B, C1], line[B1, C]]
 \[Implies] 
        collinear[P, Q, S]]

Input to the system:

Simplify[Proposition["Pappus"], by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Inserted notebook generated automatically by the system

End of inserted notebook