日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

Formalization of the Qualitative Spatial
Reasoning of Superposition of Rectangles in
Proof Assistant
Fadoua Ghourabi and Kazuko Takahashi
In qualitative spatial reasoning, objects are treated qualitatively, i.e. without performing numerical computation. In this research, we qualitatively reason about superposition of rectangles with visibility requirements.
A method is proposed to automatically superpose rectangles while respecting user’s speciﬁcation of visibility
criteria. We use proof assistant Isabelle/HOL to strengthen the proposed method. A rectangle is a resizable
object that is divided into visible regions and non-visible regions. The superposition of two rectangles iscomputed from the superposition of their regions. Rectangles are categorized into groups that are formalized as equivalence classes. Using Isabelle/HOL, we prove properties of eﬀectiveness and validity about
superposition on the equivalence classes.

spatial databases, etc. However, QSR methods rely

1 Introduction

on pen-and-paper proofs. As far as we know, there

In the 20th century, questions of mathematicalis no formal presentation of QSR methods using

rigour were throughly examined by logicians. In

proof assistants. Rigorous formalization and for-particular, the foundation of mathematical proof

mal proofs are required when we tackle some ofhas been re-examined. Pen-and-paper proofs are

QSR problems, e.g. correctness of QSR programs.

often concise and intuitive but prone to present log-

This research is an ongoing work based on theical ﬂaws, skip important steps or omit important

QSR method presented in [1]. The method deals

cases. We, therefore, became discontented to workwith the problem of superposing rectangles, calledwith a mere deﬁnition of proof. Proof assistants areunits, with requirements of visibility.

increasingly used to provide mathematical proofs

words, rectangles are spatial objects that include

where each step is transparent and, thus, the in-parts that should be visible.

volved logical reasoning can be checked.

should keep those parts visible. Possible applica-

In other

The superposition

The purpose of this research is to extend the usetion of this QSR theoretical study is the superpo-of proof assistants to provide formal proofs in qual-

sition of windows of computer software with better

itative spatial reasoning (QSR). In QSR, objects

end-user experience of visibility.

are treated qualitatively, i.e. without performing

In this research, we aim at improving the theory

numerical computation. QSR has a wide range ofof superposition of rectangles by proposing rigor-

applications in geographical information systems,

ous formalization using proof assistant. It aims at

Formalization of the Qualitative Spatial Reasoning ofSuperposition of Rectangles in Proof Assistant
Fadoua Ghourabi and Kazuko Takahashi, 関西学院大学
理工学部, School of Science and Technology, Kwansei
Gakuin University.

checking the results which were established basedon pen-and-paper proofs and revising them whennecessary. We do not create new QSR method but
rather we strengthen the formalization of an exist-

ing one using proof assistant. We choose to work

• If U has two black plates p1 and p2 , then neces-with Isabelle/HOL proof assistant [2] to formalize

sary at least one of them is of size u×h or l ×v,

the superposition of rectangles. In the rest of thewhere 0 ≤ u ≤ l and 0 ≤ v ≤ h. Furthermore,

paper, we use notations and symbols as deﬁned by

p1 and p2 must be overlapping. The overlap-

the syntax of Isabelle/HOL. We also use Isar [3]ping part forms a rectangular shared area de-framework in Isabelle/HOL. Isar provides relatively

noted by p1 u p2 (see the units in Fig. 2(c)).

structured proofs where it is possible to follow thereasoning involved in the proof. It is possible to

From the white and black plates, we compute regions.

alternate Isar proof structure with proofs adopted
in classical Isabelle/HOL.

2. 2 Regions of Unit

The rest of this paper is organized as follows.

A region can be black, white, grey, or undeﬁned.

In Sect. 2, we present a formalization of unit. In

We denote by b, w, g and N one the black, white,

Sect. 3, we deﬁne valid unit. In Sect. 4, we explain

grey and undeﬁned regions, respectively. We work

the superposition of rectangles. We prove proper-with units that are located on the 2D plane. We

ties about the results of superposition in Sect. 5

call the 2D plane the grey region. b and g regions

and we discuss the revisions that we undertook in

can be hidden while w regions should be visible.

Sect. 6. Finally, in Sect. 7, we summarize and point

In Isabelle/HOL, we deﬁne the datatype region asout directions of further research.

follows.
datatype region = None | b | w | g

2 Representation of Unit in
Isabelle/HOL
The spatial object that we investigate is a rectangle called unit. Some parts of a unit are required

For a unit U of size l × h, the regions of U are
determined as follows.
(a) Any region of U (black or white) is of sizeu × v, where 0 ≤ u ≤ l and 0 ≤ v ≤ h.

to be visible. We assume that the visible parts(b) A white plate of U is a w region.

are rectangles and model them as white rectangular(c) If p is the only black plate of U , then p isplates. The parts that can be hidden are regarded

also the only b region of U .

as black rectangular plates. We also assume that(d) If p1 and p2 are two distinct black plates

the size of a unit can change in a similar fashion toof U , then together they generate 3, 4 or 5

the way software windows are shrunk or expanded.

b regions depending on their placements (seeFig. 1). Note that the area p1 u p2 is one of the

2. 1 Black Plates
In this paper, we restrict ourselves with units
with at most two black plates. Let U be a rectangular unit of size l × h.
• If U has one black plate p, then the size ofb regions generated by p1 and p2 .
We establish a relation of adjacency on the regions of U .
Deﬁnition Two regions ri and rj of U are adjacent, denoted by ri ∼ rj , if they share an edge.

p is either l × v or u × h, where 0 ≤ u ≤ l

The values of l and h are variable. As a conse-and 0 ≤ v ≤ h. Each of the units in Fig. 3

quence, the sizes of the regions of U change while

has one black plate that is spread along thepreserving their positions in U as well as the rela-length/height of the unit.

tion ∼ and operation u.

fun up ::" representation ⇒ region"
where "up (Rep r1 r2 r3 r4) = r1"

Function regions returns the set of all the 4 regions of a representation of a unit.
fun regions::"representation ⇒region set"
where "regions U ≡ {up U, rt U, dn U, lt U}"
(a)

(b)

(c)

3 Valid Unit
図13, 4 and 5 b regions generated by two
black plates

When working with computer, we often rearrange software windows by dragging, resizing, superposing, etc. until obtaining better visibility. A

Next, we deﬁne the core of a unit.

superﬂuous information in a window, e.g. adver-Deﬁnition The core region of unit U , denoted bytisement column in a webpage, can be hidden and

CU , is a b region deﬁned as follows:

superposed by an important information in another• If U has only one b region, then CU = p.

window. The problem of arranging software win-

• If U has two distinct black plates p1 and p2 ,dows is regarded as the problem of superposing

then the core of U is the shared area between

rectangles while keeping all important information

p1 and p2 , i.e. CU = p1 u p2 .

visible. We use unit to model a software window• U has no b region, then CU is regarded as atiny b region.

and regions to specify which window parts are important, and thus, should be visible. We examine

Since a unit has at most two black plates as estab-

how applications divide the windows into regions

lished in the assumptions, then a unit has one andand, analogously, we divide units into regions. We

only one core. The unit of Fig. 2(c) has two black

restrict ourselves to unit structures that are de-plates that share a rectangular area highlighted inpicted in Fig. 2 ∼ 9.

darker black. The shared area represents the core.
We represent a unit U as sequence of 4 regions that are adjacent to CU .

We write U =hr1 , r2 , r3 , r4 i, where CU ∼ ri , 1 ≤ i ≤ 4. Regions r1 , r2 , r3 , and r4 are adjacent to CU in a clockwise order starting from the upper adjacent region.
For instance, the representations of the units in
Figs. 2(b), 3(a) and 6(a) are hw, w, w, wi, hw, g, g, gi(a) B unit(b) W unit(c) PLUS unit

and hb, g, w, bi, respectively.
datatype
representation = Rep region region region region

We deﬁne functions up, rt, dn and lt that return the upper, right, below and left adjacent regions, respectively. We show the deﬁnition of up in
Isabelle/HOL. The rest are deﬁned similarly.

図2

B, W and PLUS units

We have 3 cases of ﬁtting black plates into a unit
while respecting our assumptions in Sect. 2.
• No black plate (W type unit in Fig. 2(b))• One black plate (B, I1 and I2 type units in

(a)

(b)

(c)

(a)

(b)

(c)

(d)

図5

L1 type units(d)
図3

I1 type units

(a)
図4

(b)
(a)

(b)

(c)

(d)

I2 type units

Figs. 2(a), 3 and 4, respectively)• Two black plates (L1, L2, L3, T1, T2, PLUS
type units in Figs. 5, 6, 7, 8, 9 and 2(c), respectively)
For each unit type in Fig. 2 ∼ 9, we choose arepresentative unit as follows.
abbreviation "B ≡ Rep g g g g"
abbreviation "W ≡ Rep w w w w"
abbreviation "I1 ≡ Rep w g g g"
abbreviation "I2 ≡ Rep w g w g"
abbreviation "L1 ≡ Rep b g g b"
abbreviation "L2 ≡ Rep b g w b"
abbreviation "L3 ≡ Rep b w g b"
abbreviation "T1 ≡ Rep b b g b"
abbreviation "T2 ≡ Rep b b w b"
abbreviation "PLUS ≡ Rep b b b b"

図6

L2 type units

For instance, representative unit of I1 typeis chosen to be Rep w g g g which correspondto the unit in Fig. 3(a).

Furthermore, we in-troduce the set of representative units T 0 ={B, W, I1, I2, L1, L2, L3, T 1, T 2, P LU S}.
The units depicted in Fig. 2 ∼ 9 are called valid
units that we will deﬁne more accurately in the fol-

(a)

(b)

(c)

(d)

図7

L3 type units

(a)

(b)

(a)

(b)

(c)

(d)

図9

(a) U1
図 10

T2 type units(b) U2(c) U3

Rotations of unit U1 = hb, g, g, bi

in Fig. 10(a) is rotated to obtain U2 = hg, g, b, bi in
Fig. 10(b). We introduce function rotate to compute the rotation of a representation.

(c)

(d)

図8

T1 type units

deﬁnition rotate::"representation ⇒ representation"where"rotate U = Rep (rt U) (dn U) (lt U) (up U)"

We can carry out counter-clockwise rotation,lowing sections.

successively.

We deﬁne the recursive function

rotate succ that takes natural number n and3. 1 Rotation

return a function of type representation ⇒A unit rotation is a π2 counter-clockwise rotation.

representation. The call rotate succ n gives rise

A rotation of a unit U = hr1 , r2 , r3 , r4 i is a unit

the identity function if n = 0, otherwise n compo-

U 0 = hr2 , r3 , r4 , r1 i. For instance, U1 = hb, g, g, bi

sitions of function rotate.

Given two units U1 and U2 , the predicate
primrec rotate_succ::"nat ⇒ (representation ⇒ representation)"where"rotate_succ 0 = id"|"rotate_succ (Suc n) = rotate o rotate_succ n"

In Fig. 10, we can easily check that U2 =rotate succ 1 U1 and U3 = rotate succ 2 U1 =rotate ◦ rotate U1 .
We prove few lemmas about successive rotation.

same type returns True if U1 and U2 are of thesame type. In other words, it checks whether U2
is obtained by successive rotation of U1 . We givethe deﬁnition of same type in the following.
deﬁnition same_type::"representation ⇒ representation ⇒ bool"where"same_type U1 U2 ≡∃ n::nat. U2 = rotate_succ n U1"

These are intermediate lemmas that are used as elementary steps in more elaborate proofs. We brieﬂy
explain some of these lemmas.
If we rotate a unit U successively 4 times thenwe obtain U . We prove the following lemma to

We prove that unitrel is reﬂexive, transitive andsymmetric, and hence we deduce that unitrel is anequivalence relation.
lemma "equiv UNIV unitrel"

handle the cases where we apply n ≥ 4 successive
rotations.

Predicate equiv veriﬁes whether unitrel is anequivalence relation on the set UNIV, which is Is-

lemma rotate_succ_n:
VV" U::representation. n::nat.
rotate_succ n U = rotate_succ (n mod 4) U"

We also prove that function rotate is bijective
and invertible. The inverse function rotate−1 =rotate succ 3. Based on this result, we prove thefollowing lemma about successive rotation.
lemma rotate_succ_inverse:V
V" U1 U2:: representation. n::nat.
(rotate_succ n U1 = U2) =⇒(U1= rotate_succ (3*n) U2)"

3. 2 Equivalence Classes

abelle/HOL polymorphic constant that denotes theuniversal set. In our case the elements of UNIV areof type representation × representation.
The Isabelle/HOL expression unitrel‘‘{U } denotes the equivalence class generated by unit U ,i.e. unitrel‘‘{U }={R | (U , R) ∈ unitrel}. A
unit U is valid if and only if U is an element of theunion of the equivalence classes generated by the
representative units in T0. We have the following
deﬁnition of valid units.
deﬁnition unit :: "representation set"
whereS
"unit ≡ ( y∈T0. unitrel‘‘{y})"To compute all the units in Fig. 2 ∼ 9, we
use the formalization of equivalence classes in Isabelle/HOL [4]. We begin by deﬁning a relation
unitrel. Let U1 and U2 be two units. We have
(U1 , U2 ) ∈ unitrel if U2 is obtained by successively
rotating U1 .
deﬁnition unitrel::"(representation × representation) set"
where"unitrel ≡ {(U1, U2)| U1 U2. same_type U1 U2}"

The advantage of formalizing valid units using
Isabelle/HOL deﬁnition of equivalence classes appears when we carry out proofs of properties about
superposition of units, which will be explained further in Sect. 5.

4 Superposition of Units
We call puton the operation that performs superposition of units.

4. 1 Puton Operationcore region. We obtain a unit of type I2. Function

First, we deﬁne a partial function on that com-merge is deﬁned in Isabelle/HOL according to its
description in [1].

putes superposition of regions.
fun on:: " region ⇒where"on b b = b" |"on b w = w" |"on w b = None" |"on w w = None" |"on g g = g" |"on g x = x" |"on x g = x" |"on None _ = None"|"on _ None = None"region ⇒region"Now, superposing two units U1 and U2 by putting

(a)
図 11

(b)

Superposition and merge of I1 type unitand L3 type unit

U2 on U1 means that we put CU2 on CU1 . The coreof the resultant unit U3 is CU3 = CU2 = CU1 . Units
U1 and U2 can be resized if necessary so that the

Finally, we deﬁne the function puton that calls

cores have the same size. As explained in Sect. 2,

merge ◦ on rep.

the representation of U3 is a sequence of the re-deﬁnition puton::"representation ⇒ representation⇒ representation"
where"puton R1 R2 ≡ (if ¬(on_rep_fail R1 R2) then (merge(on_rep R1 R2)) else Undefined)"

gions that are adjacent to CU3 . Function on rep
computes the resultant unit by applying function
on on the regions of U1 and U2 .

deﬁnition on_rep::"representation ⇒ representation⇒ representation"
4. 2 Properties
where
When superposing two units, we check proper"on_rep U1 U2 ≡ties of eﬀectiveness and validity about the result(if U1=W then Undefined else
Rep (on (up U1) (up U2)) (on (rt U1) (rt U2)) (onof puton. Function puton gives rise to an eﬀective(dn U1) (dn U2)) (on (lt U1) (lt U2)))"

unit if it has at most one b region. The result ofNote that it is impossible to put any unit on W
type unit. Therefore, in that case, on rep gives riseto the Undefined unit hN one, N one, N one, N onei.
We say that on rep fails when the computed unit
has at least one N one region. We deﬁne predicate
on rep fail to check wether on call in on rep returns N one.
A function merge was introduced to obtain better
result of superposition [1]. An example of utilization of merge is depicted in Fig. 11. When we put
U2 of type I1 on U1 of type L3, part of the noncore b region of U1 is merged with CU2 to form one

puton is valid if the computed unit is valid.
deﬁnition effective::"representation ⇒ bool"where"effective R ≡ ¬ (b ∈ (regions R ))"deﬁnition valid::"representation
where "valid R ≡ R ∈ unit"⇒ bool"The eﬀectiveness and validity of the result of
operation puton are discussed in [1]. The paper
presents several general statements on these properties. Our objective is to check the correctnessof these statements by formally proving/disproving
them using Isabelle/HOL.

unitrel‘‘{P LU S}. We prove the following.

5 Theorems about Eﬀectiveness andValidity

Theorem 5.4. Superposition of a unit R on B type
unit is eﬀective if and only if R is either straight-

In Sect. 3, we explained that the units of inIs-

plate-unit or B type unit or W type unit.
∀R : representation.

abelle/HOL provides a useful predicate respect.

R ∈ SP ∪ unitrel‘‘B ∪ unitrel“W ≡terest are grouped into equivalence classes.

Let U be a unit and f be a function. f respect
unitrel‘‘{U } is true if f (Ui ) = f (Uj ) for any{Ui , Uj } ⊆ unitrel‘‘U . Therefore, from a property that respects the equivalence classes, we canbuild a proof that check properties for a representative of the equivalence class. This simpliﬁes theproofs as we don’t have to enumerate all the combinations and check the properties for all the cases,
i.e. all possible superposition of units.
We list the theorems that we proved. The detailed proofs are available online [5].

ef f ective (puton B R)
5. 2 Superposition on Straight-plate-units
Theorem 5.5. When successful, the superpositionof straight-plate-unit on a straight-plate-unit is always eﬀective.
∀R1 R2 : representation.
{R1, R2} ⊆ SP ∧ puton success R1 R2 ⇒(5)

ef f ective (puton R1 R2)Theorem 5.6. When successful, the superpositionof straight-plate-unit on straight-plate-unit is notalways valid.
∃R1 R2 : representation.
{R1, R2} ⊆ SP ∧ puton success R1 R2 ∧5. 1 Superposition on B and W TypeFor clarity, we introduce predicate puton sucessthat simply gives the negation of on rep fail.
Theorem 5.1. It is impossible to place any unit
on the W type unit in Fig. 2(b).
∀R : representation.

(4)

(6)

¬ valid (puton R1 R2)
Example Using command nitpick of Isabelle/HOL,
we generate a counter example for the formula∀R1 R2 : representation. {R1, R2} ⊆ SP ∧puton success R1 R2 ⇒ valid (puton R1 R2),

(1)

R ∈ unit ⇒ ¬ puton sucess W R
Theorem 5.2. Superposition of any unit on B typewhich is a solution for formula (6). Suppose that(see Fig. 2(a)) is always successful.
∀R : representation.

and R2 = hg, g, w, gi of type I1 (depicted in(2)
R ∈ unit ⇒ puton success B R
Theorem 5.3. Superposition of any unit on B type
unit is always valid.
∀R : representation. R ∈ unit ⇒ valid B R (3)We call straight-plate-unit a unit of I1 or I2
type depicted in Figs. 3 and 4. Cross-plate-unit
means units of types L1, L2, L3, T1, T2 and
PLUS in Figs. 5, 6, 7, 8, 9 and 2(c).

To sim-plify our formulas in the following theorems, we deﬁne the sets SP = unitrel‘‘{I1} ∪ unitrel‘‘{I2}and CP= unitrel‘‘{L1} ∪ unitrel‘‘{L2} ∪unitrel‘‘{L3} ∪ unitrel‘‘{T 1} ∪ unitrel‘‘{T 2} ∪R1 = hg, w, g, wi of type I2 (depicted in Fig. 12(a))
Fig. 12(b)). The unit in Fig. 12(b) is resized so thatits core has the same size as the core in Fig. 12(a).
Fig. 12(c) shows the result of putting R2 on R1.

5. 3 Superposition on Cross-plate-unit
Theorem 5.7. When successful, the superpositionof straight-plate-unit on a cross-plate-unit is not always eﬀective.
∃R1 R2 : representation.
R1 ∈ CP ∧ R2 ∈ SP ∧ puton success R1 R2 ∧¬ ef f ective (puton R1 R2)(7)Theorem 5.8. When successful, the superposition

(a) I2 type unit(b) I1 typeunit(a) T2 type
unit
図 13

(b) I1unit

type(c) Result ofsuperposition

Ineﬀectiveness and invalidity of

R2 = hg, g, g, wi on R1 = hb, b, w, bi

the original paper, but we choose to replace it by
successive rotations. This modiﬁcation allows simpler deﬁnition based on equivalence classes. Furthermore, in the original paper, validity property(c) Invalid
unit
図 12

Invalid unit obtained by superposing two
straight-plate-units

is judged by checking the values of the regions ofbefore and after applying puton operation. The
idea of validity property is to obtain a valid unit
by applying puton operation. We therefore simply
check that the result of puton is in the union ofof straight-plate-unit on a cross-plate-unit is not al-equivalence classes.

ways valid.
∃R1 R2 : representation.

are formalization of statements in the original pa-[Precision] The Theorems presented in Sect. 5

R1 ∈ CP ∧ R2 ∈ SP ∧ puton success R1 R2 ∧per. We provide more precise declaration of the¬ valid (puton R1 R2)properties to be proved. For instance, the origi-(8)
Example Figure 13 shows the result of putting

nal paper doesn’t explicitly specify that properties

R2 = hg, g, g, wi of type I1 on R1 = hb, b, w, bi oftype T2. The puton operation is successful but neither eﬀective nor valid.

of eﬀectiveness and validity should be checked on
successful puton operations. Unlike the prose, theformalization in Isabelle/HOL must state this condition.
[Correction] Property of validity as deﬁned in

6 Revisions[1] is wrong for some cases that were overlooked.

The new deﬁnition of validity tackles these cases
Due to the usage of proof assistant, we revised
the original QSR method presented in [1]. The revisions that we undertook are summarized in thefollowing.
[Reformulation] Only rotation is used to compute the valid unit. Reﬂection was proposed incorrectly.

Furthermore, the statement of Theo-rem 5.4 omits B and W type units. These units
should be included otherwise the theorem can not
be proved.

7 Conclusion

8 Acknowledgments

In this paper, we presented the highlight ofThis work is supported by JSPS KAKENHI

formalization of superposition of rectangles in Is-

Grant No. 25330274. The ﬁrst author is supported

abelle/HOL. We used the formalization to proveby a postdoctoral fellowship at Kwansei Gakuin

properties of eﬀectiveness and validity about the re-University.

sult of puton operation. The formalization in proof
assistant did add rigour by revealing omissions or

参 考 文 献imprecise statements in some of the deﬁnitions and[1] T. Konishi and K. Takahashi. Superposition of
Rectangles with Visibility Requirement: A Qualitative Approach. International Journal on Advancesin Software, 4(3 & 4):422–433, 2011.
[2] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order
Logic, volume 2283 of LNCS. Springer, 2002.
[3] M. Wenzel. The Isabelle/Isar Reference Manual,
2002. http://www.cl.cam.ac.uk/research/hvg/Isabelle/
dist/Isabelle2013/doc/isar-ref.pdf.
[4] L. C. Paulson. Deﬁning Functions on Equivalence Classes. ACM Transactions on Computational Logic, 7(4):658–675, 2006.
[5] F. Ghourabi. Qualitative Spatial Reasoning ofSuperposition of Rectangles - Isabelle Proofs, 2013.
http://www.i-eos.org/Members/fadoua-ghourabi.

proofs in the original work. We believe that a proposed qualitative spatial reasoning method must be
accompanied by formalization in proof assistant tounderline its accuracy and correctness.
As this is an ongoing work, we plan to extend
the formalization and add operation of embedding,which is another deﬁnition of superposition of unit.
We plan to compare the results of puton and embedding operations. We also plan to reﬁne the theorems in Sect. 5 and add general conditions to specify the cases when puton is eﬀective or valid.