Proving and Constraint Solving in Computational Origami - Artificial Intelligence and Symbolic Computation - page 139

fundamental theorems of Grobner bases theory tells us that this Grobner
basis will be iff the system is unsolvable (i.e. has no common zeros),

which was first proved in [1].

{ 1 }

5.2 Automated Proof
The proof steps would in general require laborious work of symbol manipulation.
We are developing software for performing such transformations completely au-
tomatically. The software is an extension of the geometrical theorem prover [11]
based on Theorema [2].
The following piece of programs will do all the necessary transformations and
the proof outlined above. The program will be self-explanatory, as we use the
names similar to the functions for folding used before.
The proposition to be proved is the following:

Proposition['Trisection', any[A,B,C,D,E,F,G,H,I,J,K,L,M,N],
neworigami[A,B,C,D] ∧ pon[E,line[D,C]] ∧
foldBring[A,D,crease[G on line[A,D], F on line[B,C]]] ∧
foldBring[A,G,crease[I on line[A,G], H on line[B,F]]] ∧
foldBrBr[L,A,line[H,I],N,G,line[A,E],
crease[K on line[C,D], M on line[A,B]]]

∧

⇒
equalzero[tanof[B, A, A, L] - tanof[L, A, A, J]]

symmetricPoint[J, I, line[M, K]]

∧

equalzero[tanof[B, A, A, L] - tanof[J, A, A, E]]]

KnowledgeBase['C1',any[A,B], {{ A, { 0,0 }} , { B, { 100,0 }}} ]

To display graphically the geometrical constraints among the involved
points and lines, we call function Simplify .

Simplify[Proposition['Trisection'],
by → GraphicSimplifier, using → KnowledgeBase['C1']]

The following is the output of the prover.
We have to prove:

(Proposition(Trisection))
∀
A,B,C,D,E,F,G,H,I,J,K,L,M,N

(neworigami[ A, B, C, D ] ∧ pon[ E, line [ D, C ]] ∧

foldBring[ A, D, crease[ G on line[ A, D ] ,F on line[ B, C ]]] ∧

foldBring[ A, G, crease[ I on line[ A, G ] ,H on line[ B, F ]]] ∧

foldBrBr[ L, A, line[ H, I ] ,N,G, line[ A, E ] ,
crease[ K on line[ C, D ] ,M on line[ A, B ]]]

∧

symmetricPoint[ J, I, line[ M, K ]] ⇒

equalzero[tanof[ B, A, A, L ] − tanof[ L, A, A, J ]] ∧

equalzero[tanof[ B, A, A, L ] − tanof[ J, A, A, E ]])

with no assumptions.