Research interests

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).

Tools & libraries


  • Computer science
    • Theorem proving. Ochanomizu University, Tokyo. Autumn-Winter 2016-2017 (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)

Most recent publications

  • F. Ghourabi. Allen's Interval Calculus. Archive of Formal Proofs 2016
  • F. Ghourabi, T. Ida and K. Takahashi. Interactive Construction and Automated Proof in Eos System with Application to Knot Fold of Regular Polygons. Origami6. Volume I. Mathematics, pages 55-67. American Mathematical Society, 2016.

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