Information Technology Reference
In-Depth Information
Specify the line number.
D
E
C
D
E
C
1
G
F
G
F
I
A
H
I
H
3
2
B
A
B
Step 8
Step 7
Fig. 2. Trisecting an angle by origami, steps 7-8.
Although it is not obvious to see that equational solving is performed, our
system solves a set of polynomial equations, up to the third degree. In the case
of the folds applying (O1) - (O4), the system computes a solution using the well
known mathematical formulas of elementary geometry rather than proving the
existential formulas of Axioms 1 to 4. In the case of FoldBrBr , the system solves
a cubic equation. This explains why we have (at most) 3 possible fold lines at
step 7.
5
Proof of the Correctness of the Trisection Construction
We now prove the following theorem with our system:
Theorem 1. The origami construction in section 4 trisects an angle.
5.1
Proof Method
In this simple example, the correctness of the trisection construction could be
easily verified either by geometric reasoning or by a sequence of simplification
steps of the algebraic equations representing geometric constrains. However, for
proceeding towards a general (and completely automatic) proving method for
origami theorems, we formulate the proving steps in a more general setting by
showing that the above theorem would be proved if we could show that
tan BAL =tan LAJ =tan JAE
(1)
in step 10 of Fig. 3.
A general proof procedure is as follows:
(i) We first translate the equality (1) into the algebraic form. This is done after
we fix the coordinate system (in our case Cartesian system).
Search WWH ::




Custom Search