Eos approach
What is origami geometry?
Origami is the art of paper folding. By folding a piece of paper by hand, we can make varieties of objects. The formal definition of fold operations allows making objects with meaningful geometric properties.
Why don’t you first take a tour at Eos Gallery of origami geometric objects (gallery to be prepared and link to be added)?
Why origami geometry with a program?
Let’s make your first origami geometric construction.
The above construction is self-explanatory and easy to follow (steps explained in natural English and illustrated with origami pictures, folds involved are straightforward). Things become complicated when the construction is too long and/or involves more complex fold operations. The origamist can get lost between the dozens of lines on the origami or when the descriptive captions lack accuracy. We thus need a rigorous method to describe fold operations where there is no room for confusion. Thus, the origamist would be able to focus on tasks that matter such as solving interesting origami geometric problems. In other words, through the development of Eos, we strive to make the origamist’s experience of origami geometry more compelling and painless.
The advantages of using Eos are in brief:
1) Performing folds: as mentioned above, the origamist is able to describe the fold with the rigor that is entailed in geometry. S/he delegates solving and performing the fold to a program. The key function in Eos, which allows performing folds, is called HO.
The following call of HO allows the origamist to perform common fold operations, namely Huzita and Justin fundamental operations. The parameters are existing points and lines on the origami, on which the fold is performed.
HO[<parameters of the fold operation>, <options>]
HO is general enough to allow the origamist to define his or her own fold operation. S/he can describe the geometric constraints of the fold operation in a first-order predicate logic formula, pass it to Eos and asks to process it.
HO[Constraint -> <FOL formula>, <options>]
– Designing origami constructions:
What is symbolic computation?
“(Symbolic computation) is the algorithmic treatment of all types of symbolic objects: objects in formal languages (terms, formulas, programs); algebraic objects (elements in basic number domains, polynomials, residue classes, etc.); and geometrical objects. “
from the Journal of Symbolic Computation
Why theorem proving?
Euclidean geometry: draw and prove
Correctness of the construction
Generality of the construction
Explore origami capabilities with Eos
Teach with Eos