Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL

Fadoua Ghourabi, Kazuko Takahashi

2015

Abstract

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.

Paper Citation

in Harvard Style

Ghourabi F. and Takahashi K. (2015). Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL . In Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART, ISBN 978-989-758-074-1, pages 530-539. DOI: 10.5220/0005280005300539

in Bibtex Style

@conference{icaart15,
author={Fadoua Ghourabi and Kazuko Takahashi},
title={Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL},
booktitle={Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART,},
year={2015},
pages={530-539},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005280005300539},
isbn={978-989-758-074-1},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART,
TI - Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL
SN - 978-989-758-074-1
AU - Ghourabi F.
AU - Takahashi K.
PY - 2015
SP - 530
EP - 539
DO - 10.5220/0005280005300539