Proving and constraint solving in computational origami

Origami (paper folding) has a long tradition in Japan's culture and education. We are developing a computational origami system, based on symbolic computation system Mathematica, for performing and reasoning about origami on the computer. This system is based on the implementation of the six fundamental origami folding steps (origami axioms) formulated by Huzita. In this paper, we show how our system performs origami folds by constraint solving, visualizes each step of origami construction, and automatically proves general theorems on the result of origami construction using algebraic methods. We illustrate this by a simple example of trisecting an angle by origami. The trisection of an angle is known to be impossible by means of a ruler and a compass. The entire process of computational origami shows nontrivial combination of symbolic constraint solving, theorem proving and graphical processing.