Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL
Fadoua Ghourabi, Kazuko Takahashi · 2015
We formalize and verify the superposition of rectangles in Isabelle/HOL. The superposition is associated with the arrangement of rectangular software windows while keeping some regions visible and other hidden. We adopt a qualitative spatial reasoning approach to represent these rectangles and the relations between their regions. The properties of the model are formally proved and show some characteristics of superposition operation. Although, this work is limited to 29 structures of rectangles, the superpositions produce hundreds of cases that are tedious to tackle in Isabelle/HOL. We also explain our strategy to optimize the proofs.