PD Research Report for the 2014 year
Name（Research group） Fadoua Ghourabi(Takahashi Lab, Graduate School of Science and Technology)
Research Theme

Study of Computational Models

Research PeriodApril, 2014 ~ December, 2014

Research Results（about 2,500 characters in Japanese, about 65 lines times 90 characters in English）
The purpose of this research is to formally check the correctness of qualitative spatial reasoning methods(QSR) using proof assistant. The research progress and results for the 2014 year are summarized in thefollowing.
 The formalization in Isabelle/HOL of superposition of rectangles (explained in more details in
Research Report for the 2013 year) has been completed and published in [1]. The Isabelle/HOL
theories of matrix representation of rectangle superposition are available online [4].
 The above result is limited to 29 rectangular structures. We therefore worked on overcoming
this limitation to cover superpositions of any rectangular structures, i.e. generalization of thequalitative spatial method of superposition of rectangles. The generalization requires flexible
adjustment of granularity level to establish the direction relations between regions that are notconnected. An inductive definition is given to move from one granularity level to a higher one.
As a consequence of the generalization:
The definition of expressiveness of the qualitative matrix representation is further clarified.

The notion of core is re-defined and, therefore, several solutions of superposition can becomputed.

The properties of success and effectiveness are revised accordingly.

 We are formalizing Allen's interval algebra in Isabelle/HOL and MetiTarski. The temporal
relations of Allen's interval algebra are interpreted over the field of reals. Therefore, theinterpretation is given as linear multivariate polynomial equalities and inequalities. We usedcylindrical algebraic decomposition method provided by the tool QEPCAD in MetiTarski toautomatically check the correctness of the composition table of these relations. Although
cylindrical algebraic decomposition is of higher complexity, its application to the polynomials
generated from the temporal relations terminates in a reasonable time.
 The formalization in Isabelle/HOL is also based on algebraic interpretation over the field ofreals. Axioms of Allen's interval algebra have been defined and temporal relations have beenformally deduced from them. The proofs of the properties of the axiomatic system is still inprogress, though.

List of peer-reviewed publications for the 2014 year
[1] F. Ghourabi and K. Takahashi. Formalizing the Qualitative Superposition of Rectangles in Proof
Assistant Isabelle/HOL. In Proceedings of the 7th International Conference on Agents and ArtificialIntelligence (ICAART 2015). pages 530 -- 539, Lisbon, Portugal, 2015.
[2] T. Ida, F. Ghourabi, and K. Takahashi. Formalizing Polygonal Knot Origami. Journal of SymbolicComputation. doi:10.1016/j.jsc.2014.09.031. 2014. (status: accepted and available online, September2014)

List of presentations for the 2014 year
[3] F. Ghourabi and K. Takahashi. Formalization of Matrix Representation of Direction Relations withApplications to the Superposition of rectangles. Theorem Proving and Provers metting (TPP 2014,Fukuoka)

Online publications[4] F. Ghourabi and K. Takahashi. Isabelle/HOL Theories of the Matrix Representation of Superpositionof Rectangles, November 2014. http://ist.ksc.kwansei.ac.jp/~ktaka/SuperpositionTheory/

List of planned publications[5] F. Ghourabi, T. Ida, and K. Takahashi, Automated Construction and Proving of Knot Fold by Eos
System. In Origami6: Post-proceedings of The 6th International Conference on Origami in Science,Mathematics and Education (6OSME2014), 2015. (status: will be accepted after minor modifications,January 2015)