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

K D E C

N

G F

J

I L H

A M B

Fig. 4. Graphical output of the call of Simplify .

6Con lu on

We have shown the computer origami construction with the example of trisecting
an angle. Combining the origami simulation software[10], the implementation of
the Grobner basis algorithm [1], the implementation of the decision algorithm in
Theorema [2], and a new tool [11] in Theorema , which translates the descriptions
of origami construction into the corresponding polynomial equalities, we are able
to offer a coherent tool for computational origami that can

- simulate arbitrary origami sequences both algebraically and graphically,
- translate conjectures about properties of the results of origami sequences
into statements in the form of universally quantified boolean combinations
of polynomial equalities,
- decide the truth of such conjectures and produce a proof or refutation of the
conjecture fully automatically.

We are now working to integrate those software tools into a coherent sys-
tem, each component working independently but coordinating each other on the
Internet as a symbolic computation grid.
As a next step of our research we plan to study “Origami Solving Problem”,
which asks for finding a sequence of origami steps that will lead to an origami
object with a desired property. However, it is clear that this problem is analo-
gous to the problem of finding geometric objects with desired properties using
only a ruler and a compass. Note, however, that the two problems - origami
construction and the ruler-and-compass construction - are not equivalent, as