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
- Computational origami system Eos (package and tutorial)
- Formalization of Allen's calculus (Isabelle/HOL theory file)
- 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
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