Computational origami is the computer assisted study of mathematical and computational aspects of origami. An origami is constructed by a finite sequence of fold steps, each consisting in folding along a fold line. We base the fold methods on Huzita's axiomatization, and show how folding an origami can be formulated by a conditional rewrite system. A rewriting sequence of origami structures is viewed as an ion of origami construction. We also explain how the basic concepts of constraint and functional and logic programming are related to this computational construction. Our approach is not only useful for computational construction of an origami, but it leads us to automated theorem proving of the correctness of the origami construction.