Appendix

Pappus' Theorem

Textbook formulation:

Let A B C and A1 B1 C1 be 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:

KnowledgeBase["Pappus_g", 
      any[A, B, A1, B1, C, 
        C1], {{A, {10, 120}}, {B, {100, 150}}, {A1, {25, 
            60}}, {B1,  {120, 50}}, {C, {260, 
            200}}, {C1, {250, 45}}}]

Input to the system:

Simplify[Proposition["Pappus"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Pappus_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Wu"}]

Inserted notebook generated automatically by the system

End of inserted notebook

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

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Area"}]

Inserted notebook generated automatically by the system

End of inserted notebook