Research in Computational Origami
I have been working with Prof. Ida from University of Tsukuba on developing an e-origami system, called Eos (www.i-eos.org), with the computer algebra system (CA) Mathematica. Due to relevant applications of origami in industry (e.g. Miura fold for deployment of solar arrays) and education (e.g. Haga's textbooks for origami geometry), in recent years, several systems have been designed to simulate the origami construction by hand. Eos is the 1st system that, in addition to simulation, mathematically reasons about origami geometrical constructions and proves properties about them. My main contributions to Eos project are as follows.
Logical and algebraic formalization of origami fold operations. I defined a logical and algebraic framework to describe fold operations as algebraic constraints in multi-variate polynomials over the field of origami numbers. The problem of finding a fold line that have specific geometricalproperties is therefore reduced to a constraint solving problem. The logical view and algebraic interpretation are implemented in Eos and cover, so far, Huzita's fold operations, multifold operations, circle extension and, most recently, knot fold extension.
Proving the correctness of the origami constructions. The geometrical assumptions that are automatically accumulated during the construction by Eos are employed to prove their correctness using algebraic theorem provers Groebner bases (GB) and cylindrical algebraic decomposition (CAD). Furthermore, the functionality of generating the proof document is incorporated into Eos to record the entire activities of origami construction and theorem proving.
Research in qualitative spatio-temporal reasoning
I am using proof assistant (PA) Isabelle/HOL to formalize and verify the correctness of QSTR methods.
Superposition of planar regions. The problem is about designing a systematic method to the arrangement of rectangular software windows in the plane. The arrangement involves superposition under conditions of visibility. The spatial objects of interest are rectangular structures divided into black and while regions that stand for can-be-hidden and should-be-visible parts, respectively. I use relative directions to determine how regions are positioned, and provide matrix representation to store such information. I define operations of rotation and superposition of matrices. I show how superposing rotation of matrices is equivalent to rotating the superposition of matrices. This result is relevant for optimizing the proofs of properties of superposition.
The common sense of time (or Allen's interval algebra). Qualitative composition tables, such as relation transitivity theorems of time intervals, are important to check the consistency of spatio- temporal reasoning. I verified the correctness of the composition table in Isabelle/HOL. Furthermore, I formalized the interval algebra as a type class extension of Isabelle/HOL, and properties of total strict order between events have been successfully proved.