Research interests

(1) The unifying theme of my research is theorem proving. I have been working on:

  • Correctness of qualitative spatio-temporal reasoning
  • Correctness of origami geometric constructions

Proofs of correctness is based on algebraic methods (e.g. Groebner Basis, CAD) and interactive theorem proving (i.e. proof assistant Isabelle/HOL).

(2) I am also interested in developing origami-based educational projects. Origami ought to play a role in classes of mathematics and computer science. Origami is a creative activity of geometry and designing an origami construction is a form of problem solving.

Tools & libraries

  • Computational origami system Eos (package and tutorial) I am now updating the tutorial with the new capabilities of Eos system. Hopefully, it will be published by the end of August.
  • Formalization of Allen's calculus (Isabelle/HOL theory file)


  • Computer science
    • Theorem proving. Ochanomizu University, Tokyo. Autumn-Winter 2016-2017 and Autumn-Winter 2017-2018 (course webpage)
    • Model checking, SQL language . University of Carthage, Tunisia. Autumn-Winter 2012-2013
  • Computational origami
    • DNA origami. Ochanomizu University, Tokyo. Spring 2017 (course webpage )
    • Origami mathematics & applications. Ochanomizu University, Tokyo. Summer 2015 (course webpage)
  • Others
    • Science reading, summer 2017, spring 2018
    • Science writing, winter 2017, autumn 2018

Submitted papers

2018 publications

  • F. Ghourabi and K. Takahashi. What does the qualitative spatial knowledge tell about the origami geometric folds? (accepted, to appear)
  • F. Ghourabi and K. Takahashi. A Proof of the Compositions of Time Interval Relations. CoRR abs/1804.01637, 2018.
  • F. Ghourabi. Toward non-flat geometrical origami folds Eos system. In: Proceedings of the 19th International Symposium on Symbolic and numeric Algorithms for Scientific Computing (SYNASC 2017), pages 75-79, 2018.

Contact: ghourabi "dot" fadoua "at" ocha "dot" ac "dot" jp | fadouaghourabi "at" gmail "dot" com