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

D E C D E C

G F G F

J J

I L H I L H

A B A B

Step 9 Step 10

Fig. 3. Trisecting an angle by origami, steps 9-10.

(ii) We already observed that all the folding steps are formulated in Axioms 1
- 6. These axioms are easily transcribed in terms of polynomial constraints,
once the representations of lines and points are fixed. The functions sym,
bisect, and dist, and relations

are easily defined.
(iii) We use the Grobner bases method. We collect all the premise equalities
and inequalities C =

and ⊥

{ c 1 , ..., c n } obtained at step (ii), and the conclusion

equalities and inequalities D = obtained at step (i). Let M

be the boolean combinations of the equalities and inequalities of the form
¬

{ d 1 , ..., d m }

( c 1 ∧ ... ∧ c n ) ∨ ( d 1 ∧ ... ∧ d m ), i.e. C ⇒ D .Weprove ∀ M by refutation.

The decision algorithm, roughly, proceeds as follows:
(a) Bring M into a conjunctive normal form and distribute ∀ over the con-

junctive parts. Treat each of the parts

∀
x,y,z,...

P

separately. Note that P is a disjunction

E 1 =0 ∨ ... ∨ E k =0 ∨ N 1 ∨ ... ∨ N l

=0 =0

of equalities and inequalities.
(b) Then

( E 1 =0 ∨ ... ∨ E k =0 ∨ N 1 =0 ∨ ... ∨ N l =0)

∀
x,y,z,...

is transformed into

¬ ∃
x,y,z,...

( E 1 =0 ∧ ... ∧ E k =0 ∧ N 1 =0 ∧ ... ∧ N l =0)

and further on to

¬ ( E 1 ξ 1 − 1=0 ∧ ... ∧ E k ξ k − 1=0 ∧ N 1 =0 ∧ ... ∧ N l =0)

∃
x,y,z,...,ξ 1 ,...,ξ k

with new variables ξ 1 , ..., ξ k (“Rabinovich trick”).
(c) Now, our question becomes a question on the solvability of a system of
polynomial equalities, which can be decided by computing the reduced
Grobner basis of { E 1 ξ 1 − 1 , ..., E k ξ k − 1 ,N 1 , ..., N l } . Namely, one of the