=Paper=
{{Paper
|id=None
|storemode=property
|title=The Word Problem in Semiconcept Algebras
|pdfUrl=https://ceur-ws.org/Vol-959/paper19.pdf
|volume=Vol-959
|dblpUrl=https://dblp.org/rec/conf/cla/Balbiani11
}}
==The Word Problem in Semiconcept Algebras==
https://ceur-ws.org/Vol-959/paper19.pdf
The Word Problem in Semiconcept Algebras
Philippe Balbiani
CNRS — Université de Toulouse
Institut de recherche en informatique de Toulouse
118 ROUTE DE NARBONNE, 31062 TOULOUSE CEDEX 9, France
Philippe.Balbiani@irit.fr
Abstract. The aim of this article is to prove that the word problem in
semiconcept algebras is PSPACE-complete.
Keywords: Formal concept analysis, semiconcept algebras, word problem, de-
cidability/complexity.
1 Introduction
In formal concept analysis [2, 3], the properties of formal contexts are reflected
by the properties of the concept lattices they give rise to [10, 12]. Extending
concept lattices to protoconcept algebras and semiconcept algebras, Herrmann
et al. [5] and Wille [11] introduced negations in conceptual structures based
on formal contexts such as double Boolean algebras and pure double Boolean
algebras. These algebras have attracted interest for their theoretical merits —
basic representations have been obtained — and for their practical relevance —
applications in the field of knowledge representation and reasoning have been
developed [5–7, 9, 11].
The basic representations of protoconcept algebras and semiconcept algebras
evoked above have been obtained by means of equational axioms. Hence, the
problem naturally arises of whether there is an algorithm which given terms s, t,
decides whether they represent the same element in all models of these equa-
tional axioms. Such a problem is called the word problem (WP) in protoconcept
algebras or in semiconcept algebras. In Mathematics and Computer Science,
word problems are of the utmost importance.
Within the context of protoconcept algebras, Vormbrock [8] demonstrates that
given terms s, t, if s = t is not valid in all protoconcept algebras then there
exists a finite protoconcept algebra in which s = t is not valid. Nevertheless,
the upper bound on the size of the finite protoconcept algebra given in [8, Page
258] is not elementary. Therefore, it does not allow us to conclude — as wrongly
stated in [8, Page 240] — that the WP in protoconcept algebras is NP-complete.
Switching over to semiconcept algebras, the aim of this article is to prove that
the WP in semiconcept algebras is PSPACE-complete.
Sections 2 and 3 show some of the basic properties of formal contexts and semi-
concept algebras that have been discussed in [5–7, 9, 11]. In Section 4, we present
the WP in semiconcept algebras. Section 5 introduces a basic 2-sorted modal
logic that will be used in Sections 6 and 7 to prove that the WP in semiconcept
algebras is PSPACE-complete. The proofs of Lemmas 10, 11, 12 and 13 can be
found in the annex.
2 From Formal Contexts to Semiconcept Algebras
In formal concept analysis, the properties of semiconcepts are reflected by the
properties of the algebras they give rise to.
2.1 Formal Contexts
Formal contexts are structures of the form IK = (G, M, ∆) where G is a nonempty
set (with typical member denoted g), M is a nonempty set (with typical member
denoted m) and ∆ is a binary relation between G and M . The elements of G
are called “objects”, the elements of M are called “attributes” and the intended
meaning of g ∆ m is “object g possesses attribute m”.
∆ a1 a2
o1 × ×
o2 ×
Tab. 1.
Example 1. In Tab. 1 is an example of a formal context IK2,2 with 2 objects —
o1 and o2 — and 2 attributes — a1 and a2 .
For all X ⊆ G and for all Y ⊆ M , let
X . = {m ∈ M : for all g ∈ G, if g ∈ X then g ∆ m}
Y / = {g ∈ G: for all m ∈ M , if m ∈ Y then g ∆ m}
That is to say, X . is the set of all attributes possessed by all objects in X and
Y / is the set of all objects possessing all attributes in Y .
Example 2. In the formal context IK2,2 of Tab. 1, {o1 }. = {a1 , a2 } and {a2 }/ =
{o1 }.
To carry out our plan, we need to learn a little more about the pair (. ,/ ) of
maps . : 2G 7→ 2M and / : 2M 7→ 2G . Obviously, for all X ⊆ G and for all Y ⊆
M,
– X ⊆ Y / iff X . ⊇ Y .
Hence, the pair (. ,/ ) of maps . : 2G 7→ 2M and / : 2M 7→ 2G is a Galois connection
between (2G , ⊆) and (2M , ⊇). Thus, for all X, X1 , X2 ⊆ G and for all Y, Y1 , Y2
⊆ M,
– if X1 ⊆ X2 then X1. ⊇ X2. ,
– if Y1 ⊇ Y2 then Y1/ ⊆ Y2/ ,
– X ⊆ X ./ and X . = X ./. ,
– Y /. ⊇ Y and Y / = Y /./ .
2.2 Semiconcept Algebras
Let IK = (G, M, ∆) be a formal context. Given X ⊆ G, the pair (X, X . ) is called
“left semiconcept of IK”. Remark that (∅, M ) is a left semiconcept of IK. Let
Hl (IK) = (Hl (IK), ⊥l , >l , ¬l , ∨l , ∧l )
be the algebraic structure of type (0, 0, 1, 2, 2) where Hl (IK) is the set of all left
semiconcepts of IK, ⊥l = (∅, M ), >l = (G, G. ), ¬l (X, X . ) = (G \ X, (G \ X). ),
(X1 , X1. ) ∨l (X2 , X2. ) = (X1 ∪ X2 , (X1 ∪ X2 ). ) and (X1 , X1. ) ∧l (X2 , X2. ) = (X1 ∩
X2 , (X1 ∩X2 ). ). Remark that if G is finite then Hl (IK) is finite too and moreover,
| Hl (IK) | = 2|G| . It is a simple exercise to check that the above operations ⊥l ,
>l , ¬l ·, · ∨l · and · ∧l · on Hl (IK) are isomorphic to the Boolean operations ∅, G,
G \ ·, · ∪ · and · ∩ · on 2G . Hence, Hl (IK) satisfies the conditions of nondegenerate
Boolean algebras. Given Y ⊆ M , the pair (Y / , Y ) is called “right semiconcept
of IK”. Remark that (G, ∅) is a right semiconcept of IK. Let
Hr (IK) = (Hr (IK), ⊥r , >r , ¬r , ∨r , ∧r )
be the algebraic structure of type (0, 0, 1, 2, 2) where Hr (IK) is the set of all right
semiconcepts of IK, ⊥r = (M / , M ), >r = (G, ∅), ¬r (Y / , Y ) = ((M \Y )/ , M \Y ),
(Y1/ , Y1 ) ∨r (Y2/ , Y2 ) = ((Y1 ∩ Y2 )/ , Y1 ∩ Y2 ) and (Y1/ , Y1 ) ∧r (Y2/ , Y2 ) = ((Y1 ∪
Y2 )/ , Y1 ∪ Y2 ). Remark that if M is finite then Hr (IK) is finite too and moreover,
| Hr (IK) | = 2|M | . It is a simple exercise to check that the above operations
⊥r , >r , ¬r ·, · ∨r · and · ∧r · on Hr (IK) are anti-isomorphic to the Boolean
operations ∅, M , M \·, ·∪· and ·∩· on 2M . Hence, Hr (IK) satisfies the conditions
of nondegenerate Boolean algebras. Now, for the concept underlying most of
our work in this article. Given X ⊆ G and Y ⊆ M , the pair (X, Y ) is called
“semiconcept of IK” iff Y = X . or X = Y / . Remark that (∅, M ) and (G, ∅) are
semiconcepts of IK.
Example 3. In the formal context IK2,2 of Tab. 1, the semiconcepts are (∅, {a1 ,
a2 }), ({o1 }, {a1 , a2 }), ({o2 }, {a1 }), ({o1 }, {a2 }), ({o1 , o2 }, {a1 }) and ({o1 , o2 }, ∅).
Let
H(IK) = (H(IK), ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l , ∧r )
be the algebraic structure of type (0, 0, 0, 0, 1, 1, 2, 2, 2, 2) where H(IK) is the set
of all semiconcepts of IK, ⊥l = (∅, M ), ⊥r = (M / , M ), >l = (G, G. ), >r = (G, ∅),
¬l (X, Y ) = (G \ X, (G \ X). ), ¬r (X, Y ) = ((M \ Y )/ , M \ Y ), (X1 , Y1 ) ∨l (X2 , Y2 )
= (X1 ∪ X2 , (X1 ∪ X2 ). ), (X1 , Y1 ) ∨r (X2 , Y2 ) = ((Y1 ∩ Y2 )/ , Y1 ∩ Y2 ), (X1 , Y1 ) ∧l
(X2 , Y2 ) = (X1 ∩ X2 , (X1 ∩ X2 ). ) and (X1 , Y1 ) ∧r (X2 , Y2 ) = ((Y1 ∪ Y2 )/ , Y1 ∪ Y2 ).
Example 4. In the formal context IK2,2 of Tab. 1, ⊥l = (∅, {a1 , a2 }), >l =
({o1 , o2 }, {a1 }), ⊥r = ({o1 }, {a1 , a2 }) and >r = ({o1 , o2 }, ∅).
Remark that if G, M are finite then H(IK) is finite too and moreover, | H(IK) | ≤
2|G| + 2|M | . Obviously, the operations ⊥l , >l , ¬l ·, · ∨l · and · ∧l ·, when restricted
to the set of all left semiconcepts of IK, are isomorphic to the Boolean operations
∅, G, G \ ·, · ∪ · and · ∩ · on 2G whereas the operations ⊥r , >r , ¬r ·, · ∨r · and · ∧r ·,
when restricted to the set of all right semiconcepts of IK, are anti-isomorphic to
the Boolean operations ∅, M , M \ ·, · ∪ · and · ∩ · on 2M . In other respects, it is
a simple matter to check that H(IK) satisfies the following conditions for every
x, y, z ∈ H(IK):
– x ∧l (y ∧l z) = (x ∧l y) ∧l z and x ∨r (y ∨r z) = (x ∨r y) ∨r z,
– x ∧l y = y ∧l x and x ∨r y = y ∨r x,
– ¬l (x ∧l x) = ¬l x and ¬r (x ∨r x) = ¬r x,
– x ∧l (y ∧l y) = x ∧l y and x ∨r (y ∨r y) = x ∨r y,
– x ∧l (y ∨l z) = (x ∧l y) ∨l (x ∧l z) and x ∨r (y ∧r z) = (x ∨r y) ∧r (x ∨r z),
– x ∧l (x ∨l y) = x ∧l x and x ∨r (x ∧r y) = x ∨r x,
– x ∧l (x ∨r y) = x ∧l x and x ∨r (x ∧l y) = x ∨r x,
– ¬l (¬l x ∧l ¬l y) = x ∨l y and ¬r (¬r x ∨r ¬r y) = x ∧r y,
– ¬l ⊥l = >l and ¬r >r = ⊥r ,
– ¬l >r = ⊥l and ¬r ⊥l = >r ,
– >r ∧l >r = >l and ⊥l ∨r ⊥l = ⊥r ,
– x ∧l ¬l x = ⊥l and x ∨r ¬r x = >r ,
– ¬l ¬l (x ∧l y) = x ∧l y and ¬r ¬r (x ∨r y) = x ∨r y,
– (x ∧l x) ∨r (x ∧l x) = (x ∨r x) ∧l (x ∨r x),
– x ∧l x = x or x ∨r x = x.
Let us remark that the first 13 above conditions come in pairs of mirror images
obtained by interchanging ⊥l with >r , >l with ⊥r , ¬l with ¬r , ∨l with ∧r
and ∧l with ∨r whereas the last 2 above conditions are equivalent to their own
mirror images. This leads us to the principle of duality stating that from any
condition provable from the 15 above conditions, another such condition results
immediately by interchanging ⊥l with >r , >l with ⊥r , ¬l with ¬r , ∨l with ∧r
and ∧l with ∨r . The set H(IK) can be ordered by the binary relation v defined
by
(X1 , Y1 ) v (X2 , Y2 ) iff X1 ⊆ X2 and Y1 ⊇ Y2
for every (X1 , Y1 ), (X2 , Y2 ) ∈ H(IK). Obviously, for all (X1 , Y1 ), (X2 , Y2 ) ∈
H(IK),
– (X1 , Y1 ) v (X2 , Y2 ) iff (X1 , Y1 )∧l (X2 , Y2 ) = (X1 , Y1 )∧l (X1 , Y1 ) and (X1 , Y1 )
∨r (X2 , Y2 ) = (X2 , Y2 ) ∨r (X2 , Y2 ),
– if (X1 , Y1 ) ∈ Hl (IK) then (X1 , Y1 ) v (X2 , Y2 ) iff (X1 , Y1 ) ∧l (X2 , Y2 ) =
(X1 , Y1 ),
– if (X2 , Y2 ) ∈ Hr (IK) then (X1 , Y1 ) v (X2 , Y2 ) iff (X1 , Y1 ) ∨r (X2 , Y2 ) =
(X2 , Y2 ).
Moreover, the binary relation v is reflexive, antisymmetric and transitive on
H(IK). In order to give an abstract characterization of the operations ⊥l , ⊥r ,
>l , >r , ¬l , ¬r , ∨l , ∨r , ∧l and ∧r , we shall say that an algebraic structure D =
(D, ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l , ∧r ) of type (0, 0, 0, 0, 1, 1, 2, 2, 2, 2) is a pure
double Boolean algebra iff the operations ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l and
∧r satisfy the 15 above conditions.
3 From Semiconcept Algebras to Formal Contexts
The aim of this section is to give an abstract characterization of the operations
⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l and ∧r .
3.1 Filters and Ideals
Let D = (D, ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l , ∧r ) be a pure double Boolean alge-
bra. We define
Dl = {x ∧l x: x ∈ D}
Dr = {x ∨r x: x ∈ D}
Intuitively, elements of Dl can be considered as sets of objects and elements of
Dr can be considered as sets of attributes.
Example 5. In the semiconcept algebra associated to the formal context IK2,2 of
Tab. 1, D2,2 = {(∅, {a1 , a2 }), ({o1 }, {a1 , a2 }), ({o2 }, {a1 }), ({o1 }, {a2 }), ({o1 , o2 },
{a1 }), ({o1 , o2 }, ∅)}, Dl2,2 = {(∅, {a1 , a2 }), ({o1 }, {a1 , a2 }), ({o2 }, {a1 }), ({o1 , o2 },
{a1 })} and Dr2,2 = {({o1 }, {a1 , a2 }), ({o1 , o2 }, {a1 }), ({o1 }, {a2 }), ({o1 , o2 }, ∅)}.
Obviously, the operations ⊥l , >l , ¬l , ∨l and ∧l are stable on Dl and the opera-
tions ⊥r , >r , ¬r , ∨r and ∧r are stable on Dr . Hence, the algebraic structures Dl
= (Dl , ⊥l , >l , ¬l , ∨l , ∧l ) and Dr = (Dr , ⊥r , >r , ¬r , ∨r , ∧r ) are algebraic struc-
tures of type (0, 0, 1, 2, 2). More precisely, they are Boolean algebras. Moreover,
the set D can be ordered by the binary relation ≤ defined by
x ≤ y iff x ∧l y = x ∧l x and x ∨r y = y ∨r y
for every x, y ∈ D. Obviously, for all x, y ∈ D,
– if x ∈ Dl then x ≤ y iff x ∧l y = x,
– if y ∈ Dr then x ≤ y iff x ∨r y = y.
Moreover, the binary relation ≤ is reflexive, antisymmetric and transitive on D.
({o1 , o2 }, ∅)
q
@ I @
({o1 }, {a2 })@ ({o1 , o2 }, {a1 })
q @q
I
@ @ @ I@
@ ({o1 }, {a1 , a@ 2 }) ({o2 }, {a1 })
@q @q
I
@ @
@ (∅, {a1 , a2 })
@q
Fig. 1.
Example 6. In Fig. 1 is represented the binary relation ≤2,2 ordering the set
D2,2 of the semiconcept algebra associated to the formal context IK2,2 of Tab. 1.
A nonempty subset F of D is called a filter iff for all x, y ∈ D,
– x, y ∈ F implies x ∧l y ∈ F ,
– x ∈ F and x ≤ y imply y ∈ F .
A nonempty subset I of D is called an ideal iff for all x, y ∈ D,
– x, y ∈ I implies x ∨r y ∈ I,
– x ∈ I and y ≤ x imply y ∈ I.
The following lemma explains how filters and ideals can be transformed into
filters and ideals of the Boolean algebras Dl and Dr .
Lemma 1. Let F, I be nonempty subsets of D. If F is a filter then F ∩ Dl is a
filter of the Boolean algebra Dl and F ∩ Dr is a filter of the Boolean algebra Dr
and if I is an ideal then I ∩ Dl is an ideal of the Boolean algebra Dl and I ∩ Dr
is an ideal of the Boolean algebra Dr .
Let F be a nonempty subset of Dl and I be a nonempty subset of Dr . We define
[F ) = {x ∈ D: there exists y ∈ F such that y ≤ x}
(I] = {x ∈ D: there exists y ∈ I such that x ≤ y}
The following lemma explains how filters of the Boolean algebra Dl and ideals
of the Boolean algebra Dr can be transformed into filters and ideals.
Lemma 2. Let F be a nonempty subset of Dl , I be a nonempty subset of Dr .
If F is a filter of the Boolean algebra Dl then [F ) is a filter and [F ) ∩ Dl = F
and if I is an ideal of the Boolean algebra Dr then (I] is an ideal and (I] ∩ Dr
= I.
As a result,
Lemma 3. There exists filters F such that F ∩Dl is a prime filter of the Boolean
algebra Dl and there exists ideals I such that I∩Dr is a prime ideal of the Boolean
algebra Dr .
We shall say that D is concrete iff there exists a formal context IK and a function
h assigning to each element of D an element of H(IK) such that h is injective
and h is a homomorphism from D to H(IK).
3.2 Representation
Now, the main question is to prove that every pure double Boolean algebra
is concrete. Let D = (D, ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l , ∧r ) be a pure double
Boolean algebra and consider the formal context
IK(D) = (Fp (D), Ip (D), ∆)
where Fp (D) is the set of all filters F for which F ∩ Dl is a prime filter of the
Boolean algebra Dl , Ip (D) is the set of all ideals I for which I ∩ Dr is a prime
ideal of the Boolean algebra Dr and F ∆ I iff F ∩ I is nonempty. Let
H(IK(D)) = (H(IK(D)), ⊥0l , ⊥0r , >0l , >0r , ¬0l , ¬0r , ∨0l , ∨0r , ∧0l , ∧0r )
For all elements x of D, let
Fx = {F ∈ Fp (D): x ∈ F }
Ix = {I ∈ Ip (D): x ∈ I}
Here, the first results are
Lemma 4. Let x ∈ D. Fx∧l x = Fx and Ix∨r x = Ix .
Lemma 5. Let x ∈ D. If x ∈ Dl then Fx. = Ix and if x ∈ Dr then Ix/ = Fx .
Lemma 6. Let x ∈ D. F¬.l ¬l x = I¬l ¬l x and I¬/ r ¬r x = F¬r ¬r x .
The next lemmas point the way to the strategy followed in our approach to the
proof that every pure double Boolean algebra is concrete.
Lemma 7. Let x ∈ D. The pair (Fx , Ix ) is a semiconcept of IK(D).
Lemma 8. Let x, y ∈ D. If x 6= y then (Fx , Ix ) 6= (Fy , Iy ).
For all x ∈ D, let
h(x) = (Fx , Ix )
The next lemma is central for proving that the function h is a homomorphism
from D to H(IK).
Lemma 9. Let x, y ∈ D.
– F⊥l = ∅ and I⊥l = Ip (D),
– F⊥r = Ip (D)/ and I⊥r = Ip (D),
– F>l = Fp (D) and I>l = Fp (D). ,
– F>r = Fp (D) and I>r = ∅,
– F¬l x = Fp (D) \ Fx and I¬l x = (Fp (D) \ Fx ). ,
– F¬r x = (Ip (D) \ Ix )/ and I¬r x = Ip (D) \ Ix ,
– Fx∨l y = Fx ∪ Fy and Ix∨l y = (Fx ∪ Fy ). ,
– Fx∨r y = (Ix ∩ Iy )/ and Ix∨r y = Ix ∩ Iy ,
– Fx∧l y = Fx ∩ Fy and Ix∧l y = (Fx ∩ Fy ). ,
– Fx∧r y = (Ix ∪ Iy )/ and Ix∧r y = Ix ∪ Iy .
As a result,
Theorem 1. The function h is a homomorphism from D to H(IK).
In other words: every pure double Boolean algebra is concrete.
4 The Word Problem in Pure Double Boolean Algebras
Let us introduce the word problem in pure double Boolean algebras.
4.1 Syntax
Let V ar denote a countable set of individual variables (with typical instances
denoted x, y, etc). The set t(V ar) of all terms (with typical instances denoted
s, t, etc) is given by the rule
s ::= x | 0l | 0r | 1l | 1r | −l s | −r s | (s tl t) | (s tr t) | (s ul t) | (s ur t)
Let us adopt the standard rules for omission of the parentheses.
Example 7. For instance, x ul (x tr y) is a term.
4.2 Semantics
Let D = (D, ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r , ∧l , ∧r ) be a pure double Boolean alge-
bra. A valuation based on D is a function m assigning to each individual variable
x an element m(x) of D.
Example 8. The function m2,2 defined below is a valuation based on the pure
double Boolean algebra D2,2 defined in Example 5: m2,2 (x) = ({o2 }, {a1 }),
m2,2 (y) = ({o1 }, {a2 }) and for all individual variables z, if z 6= x, y then m2,2 (z)
= ({o1 , o2 }, {a1 }).
m induces a function (·)m assigning to each term s an element (s)m of D such
that (x)m = m(x), (0l )m = ⊥l , (0r )m = ⊥r , (1l )m = >l , (1r )m = >r , (−l s)m
= ¬l (s)m , (−r s)m = ¬r (s)m , (s tl t)m = (s)m ∨l (t)m , (s tr t)m = (s)m ∨r (t)m ,
(s ul t)m = (s)m ∧l (t)m and (s ur t)m = (s)m ∧r (t)m .
Example 9. Concerning the valuation m2,2 defined in Example 8, we have (x tr
2,2 2,2
y)m = ({o1 , o2 }, ∅) and (−l x)m = ({o1 }, {a1 , a2 }).
4.3 The Word Problem
Now, for the WP in pure double Boolean algebras:
input: terms s, t,
output: determine whether there exists a pure double Boolean algebra D and
a valuation m based on D such that (s)m 6= (t)m .
A general strategy for proving a decision problem to be PSPACE-complete is
first, to reduce to it a decision problem easily proved to be PSPACE-hard and
second, to reduce it to a decision problem easily proved to be in PSPACE.
PSPACE is the key complexity class of the satisfiability problem of numerous
modal logics [1, Chapter 6]. Therefore, we introduce in Section 5 a PSPACE-
complete modal logic and we show in Sections 6 and 7 how to reduce one into
the other its satisfiability problem and the WP in pure double Boolean algebras.
5 A Basic 2-Sorted Modal Logic
In Section 3, we gave the proof that every pure double Boolean algebra can
be homomorphically embedded into the pure double Boolean algebra over some
formal context. Formal contexts are 2-sorted structures. Hence, the modal logic
that will be used in Sections 6 and 7 for proving the WP in pure double Boolean
algebras to be PSPACE-complete is a 2-sorted one.
5.1 Syntax
The language of K2 is based on a countable set OV ar of object variables (with
typical instances denoted P , Q, etc) and a countable set AV ar of attribute
variables (with typical instances denoted p, q, etc). Without loss of generality,
let us assume that OV ar and AV ar are disjoint. The set of all object formulas
(with typical instances denoted A, B, etc) and the set of all attribute formulas
(with typical instances denoted a, b, etc) are given by the rules
A ::= P | ⊥ | ¬A | (A ∨ B) | 2a
a ::= p | ⊥ | ¬a | (a ∨ b) | 2A
The other Boolean constructs are defined as usual. Let us adopt the standard
rules for omission of the parentheses. A formula (with typical instances denoted
α, β, etc) is either an object formula or an attribute formula. The notion of
“being a subformula of” is standard, the expression α β denoting the fact
that α is a subformula of β. A substitution is a pair (Θ, θ) where Θ is a function
assigning to each object variable P an object formula Θ(P ) and θ is a function
assigning to each attribute variable p an attribute formula θ(p). (Θ, θ) induces a
homomorphism (·)(Θ,θ) assigning to each formula α a formula (α)(Θ,θ) such that
(P )(Θ,θ) = Θ(P ) and (p)(Θ,θ) = θ(p). Remark that for all object formulas A and
for all attribute formulas a,
– (A)(Θ,θ) is an object formula,
– (a)(Θ,θ) is an attribute formula.
Let OV ar = P1 , P2 , . . . be an enumeration of OV ar and AV ar = p1 , p2 , . . . be
an enumeration of AV ar. We shall say that a substitution (Θ, θ) is normal with
respect to OV ar and AV ar iff for all positive integers i,
– Θ(Pi ) = Pi and θ(pi ) = 2Pi or Θ(Pi ) = 2pi and θ(pi ) = pi .
Given a formula α, V ar(α) will denote the set of all variables occurring in α. A
formula α is said to be nice iff
– V ar(α) ⊆ OV ar or V ar(α) ⊆ AV ar.
5.2 Semantics
Let IK = (G, M, ∆) be a formal context. A IK-valuation is a pair (V, v) of func-
tions where V assigns to each object variable P a subset V (P ) of G and v assigns
to each attribute variable p a subset v(p) of M . (V, v) induces a function (·)(V,v)
assigning to each formula α a subset (α)(V,v) of G ∪ M such that (P )(V,v) =
V (P ), (⊥)(V,v) = ∅, (¬A)(V,v) = G \ (A)(V,v) , (A ∨ B)(V,v) = (A)(V,v) ∪ (B)(V,v) ,
(2a)(V,v) = {g ∈ G: for all m ∈ M , if m ∈ (a)(V,v) then g ∆ m}, (p)(V,v) =
v(p), (⊥)(V,v) = ∅, (¬a)(V,v) = M \ (a)(V,v) , (a ∨ b)(V,v) = (a)(V,v) ∪ (b)(V,v) and
(2A)(V,v) = {m ∈ M : for all g ∈ G, if g ∈ (A)(V,v) then g ∆ m}. Remark that
for all object formulas A and for all attribute formulas a,
.
– (A)(V,v) is a subset of G such that (A)(V,v) = (2A)(V,v) ,
/
– (a)(V,v) is a subset of M such that (a)(V,v) = (2a)(V,v) .
A formula α is said to be satisfiable iff
– there exists a formal context IK = (G, M, ∆) and a IK-valuation (V, v) such
that (α)(V,v) is nonempty.
5.3 Decision
Now, for the nice satisfiability problem for K2 :
input: a nice formula α,
output: determine whether α is satisfiable.
The next lemmas are central for proving that the problem of deciding equations
in pure double Boolean algebras is PSPACE-complete.
Theorem 2. The nice satisfiability problem for K2 is PSPACE-hard.
Proof. A reduction similar to the reduction from the QBF -validity problem to
the satisfiability problem for K considered in [1, Theorem 6.50] can be easily
obtained.
Now, for the satisfiability problem for K2 :
input: a formula α,
output: determine whether α is satisfiable.
Theorem 3. The satisfiability problem for K2 is in PSPACE.
Proof. An algorithm similar to the W itness algorithm considered in [1, Theorem
6.47] can be easily obtained.
From Theorems 2 and 3, it follows immediately that the nice satisfiability prob-
lem for K2 and the satisfiability problem for K2 are both PSPACE-complete.
6 From K2 to Pure Double Boolean Algebras
First, we consider the lower bound of the complexity of the problem of deciding
the WP in pure double Boolean algebras. Given a nice formula α, we wish to
construct a pair (s1 (α), s2 (α)) of terms such that α is satisfiable iff there exists
a pure double Boolean algebra D and a valuation m based on D such that
(s1 (α))m 6= (s2 (α))m . Let OV ar = P1 , P2 , . . . be an enumeration of OV ar,
AV ar = p1 , p2 , . . . be an enumeration of AV ar and V ar = x1 , y1 , x2 , y2 , . . . be
an enumeration of V ar. The function T (·) assigning to each nice object formula
A a term T (A) and the function t(·) assigning to each nice attribute formula a a
term t(a) are such that T (Pi ) = xi , T (⊥) = 0l , T (¬A) = −l T (A), T (A ∨ B) =
T (A) tl T (B), T (2a) = −l −l −r −r t(a), t(pi ) = yi , t(⊥) = 1r , t(¬a) = −r t(a),
t(a ∨ b) = t(a) ur t(b) and t(2A) = −r −r −l −l T (A). Let (s1 (·), s2 (·)) be the
function assigning to each nice formula α a pair (s1 (α), s2 (α)) of terms such that
if α is a nice object formula then s1 (α) = T (α) and s2 (α) = 0l and if α is a nice
attribute formula then s1 (α) = t(α) and s2 (α) = 1r . Obviously, (s1 (α), s2 (α))
can be computed in space log | α |. Moreover,
Proposition 1. If α is nice then α is satisfiable iff there exists a pure double
Boolean algebra D and a valuation m based on D such that (s1 (α))m 6= (s2 (α))m .
Proof. Since α is nice, V ar(α) ⊆ OV ar or V ar(α) ⊆ AV ar. Without loss of
generality, let us assume that V ar(α) ⊆ OV ar. Hence, there exists a positive
integer n such that V ar(α) ⊆ {P1 , . . . , Pn }.
(⇒) Suppose α is satisfiable, we demonstrate there exists a pure double Boolean
algebra D and a valuation m based on D such that (s1 (α))m 6= (s2 (α))m . Since α
is satisfiable, there exists a formal context IK = (G, M, ∆) and a valuation (V, v)
based on IK such that (α)(V,v) is nonempty. Let H(IK) = (H(IK), ⊥l , ⊥r , >l , >r ,
¬l , ¬r , ∨l , ∨r , ∧l , ∧r ) and m be a valuation based on H(IK) such that for all
positive integers i, if i ≤ n then m(xi ) = (V (Pi ), V (Pi ). ). We show first that
Lemma 10. Let A be a nice object formula and a be a nice attribute formula.
.
If A α then (T (A))m = ((A)(V,v) , (A)(V,v) ) and if a α then (t(a))m =
/
((a)(V,v) , (a)(V,v) ).
Continuing the proof of Proposition 1, since (α)(V,v) is nonempty, by Lemma 10,
if α is a nice object formula then (T (α))m 6= (0l )m and if α is a nice attribute
formula then (t(α))m 6= (1r )m . Hence, (s1 (α))m 6= (s2 (α))m . Thus, there exists a
pure double Boolean algebra D and a valuation m based on D such that (s1 (α))m
6= (s2 (α))m .
(⇐) Suppose there exists a pure double Boolean algebra D and a valuation m
based on D such that (s1 (α))m 6= (s2 (α))m , we demonstrate α is satisfiable. Let
IK(D) = (Fp (D), Ip (D), ∆) and (V, v) be a valuation based on IK(D) such that
for all positive integers i, if i ≤ n then V (Pi ) = Fm(xi ) . Interestingly,
Lemma 11. Let A be a nice object formula and a be a nice attribute formula.
If A α then (A)(V,v) = F(T (A))m and if a α then (a)(V,v) = I(t(a))m .
Continuing the proof of Proposition 1, since (s1 (α))m 6= (s2 (α))m , if α is a
nice object formula then (T (α))m 6= (0l )m and if α is a nice attribute formula
then (t(α))m 6= (1r )m . Hence, by Lemma 11, (α)(V,v) is nonempty. Thus, α is
satisfiable. This ends the proof of Proposition 1.
Hence, (s1 (·), s2 (·)) is a reduction from the nice satisfiability problem for K2 to
the WP in pure double Boolean algebras. Thus, by Theorem 2,
Corollary 1. The WP in pure double Boolean algebras is PSPACE-hard.
7 From Pure Double Boolean Algebras to K2
Second, we consider the upper bound of the complexity of the WP in pure double
Boolean algebras. Given a pair (s, t) of terms, we wish to construct an object
formula O(s, t) and an attribute formula A(s, t) such that there exists a pure
double Boolean algebra D and a valuation m based on D such that (s)m 6= (t)m
iff some instance of O(s, t) is satisfiable or some instance of A(s, t) is satisfiable.
Let V ar = x1 , x2 , . . . be an enumeration of V ar, OV ar = P1 , P2 , . . . be an
enumeration of OV ar and AV ar = p1 , p2 , . . . be an enumeration of AV ar. The
function F (·) assigning to each term s an object formula F (s) and the function
f (·) assigning to each term s an attribute formula f (s) are such that F (xi ) = Pi ,
f (xi ) = pi , F (0l ) = ⊥, f (0l ) = 2⊥, F (0r ) = 2>, f (0r ) = >, F (1l ) = >, f (1l )
= 2>, F (1r ) = 2⊥, f (1r ) = ⊥, F (−l s) = ¬F (s), f (−l s) = 2¬F (s), F (−r s) =
2¬f (s), f (−r s) = ¬f (s), F (s tl t) = F (s) ∨ F (t), f (s tl t) = 2(F (s) ∨ F (t)),
F (str t) = 2(f (s)∧f (t)), f (str t) = f (s)∧f (t), F (sul t) = F (s)∧F (t), f (sul t) =
2(F (s)∧F (t)), F (sur t) = 2(f (s)∨f (t)) and f (sur t) = f (s)∨f (t). Let O(·, ·) be
the function assigning to each pair (s, t) of terms the object formula O(s, t) such
that O(s, t) = ¬(F (s) ↔ F (t)). Let A(·, ·) be the function assigning to each pair
(s, t) of terms the attribute formula A(s, t) such that A(s, t) = ¬(f (s) ↔ f (t)).
Obviously, O(s, t) and A(s, t) can be computed in space log | (s, t) |. Moreover,
Proposition 2. There exists a pure double Boolean algebra D and a valuation
m based on D such that (s)m 6= (t)m iff there exists a substitution (Θ, θ) such that
(Θ, θ) is normal with respect to OV ar and AV ar and O(s, t)(Θ,θ) is satisfiable
or A(s, t)(Θ,θ) is satisfiable.
Proof. Let n be a positive integer such that V ar(s) ∪ V ar(t) ⊆ {x1 , . . . , xn }.
(⇒) Suppose there exists a pure double Boolean algebra D and a valuation m
based on D such that (s)m 6= (t)m , we demonstrate there exists a substitu-
tion (Θ, θ) such that (Θ, θ) is normal with respect to OV ar and AV ar and
O(s, t)(Θ,θ) is satisfiable or A(s, t)(Θ,θ) is satisfiable. Let (Θ, θ) be a normal sub-
stitution with respect to OV ar and AV ar such that for all positive integers i,
if i ≤ n then if m(xi ) is in Dl then Θ(Pi ) = Pi and θ(pi ) = 2Pi and if m(xi )
is in Dr then Θ(Pi ) = 2pi and θ(pi ) = pi . Let IK(D) = (Fp (D), Ip (D), ∆) and
(V, v) be a valuation based on IK(D) such that for all positive integers i, if i ≤ n
then V (Pi ) = Fm(xi ) and v(pi ) = Im(xi ) . Remark that for all positive integers i,
(V,v)
if i ≤ n then if m(xi ) is in Dl then (Pi )(Θ,θ) = (Pi )(V,v) = V (Pi ) = Fm(xi )
(V,v) /
and if m(xi ) is in Dr then (Pi )(Θ,θ) = (2pi )(V,v) = (pi )(V,v) = v(pi )/ =
/
Im(xi ) = Fm(xi ) . Similarly, for all positive integers i, if i ≤ n then if m(xi ) is in
(V,v) .
Dl then (pi )(Θ,θ) = (2Pi )(V,v) = (Pi )(V,v) = V (Pi ). = Fm(x
.
i)
= Im(xi ) and
(V,v)
if m(xi ) is in Dr then (pi )(Θ,θ) = (pi )(V,v) = v(pi ) = Im(xi ) We first observe
(V,v)
Lemma 12. Let u be a term. If u s or u t then (F (u))(Θ,θ) = F(u)m
(Θ,θ) (V,v)
and (f (u)) = I(u)m .
Continuing the proof of Proposition 2, since (s)m 6= (t)m , F(s)m 6= F(t)m or I(s)m
(V,v) (V,v)
6 I(t)m . Hence, by Lemma 12, O(s, t)(Θ,θ)
= is nonempty or A(s, t)(Θ,θ)
is nonempty. Thus, there exists a substitution (Θ, θ) such that (Θ, θ) is normal
with respect to OV ar and AV ar and O(s, t)(Θ,θ) is satisfiable or A(s, t)(Θ,θ)
is satisfiable.
(⇐) Suppose there exists a substitution (Θ, θ) such that (Θ, θ) is normal with
respect to OV ar and AV ar and O(s, t)(Θ,θ) is satisfiable or A(s, t)(Θ,θ) is sat-
isfiable, we demonstrate there exists a pure double Boolean algebra D and a
valuation m based on D such that (s)m 6= (t)m . Since O(s, t)(Θ,θ) is satisfi-
able or A(s, t)(Θ,θ) is satisfiable, there exists a formal context IK = (G, M, ∆)
(V,v)
and a valuation (V, v) based on IK such that O(s, t)(Θ,θ) is nonempty or
(V,v)
A(s, t)(Θ,θ) is nonempty. Let H(IK) = (H(IK), ⊥l , ⊥r , >l , >r , ¬l , ¬r , ∨l , ∨r ,
∧l , ∧r ) and m be a valuation based on H(IK) such that for all positive integers
i, if i ≤ n then m(xi ) = ((Θ(Pi ))(V,v) , (θ(pi ))(V,v) ). Interestingly,
(V,v)
Lemma 13. Let u be a term. If u s or u t then (u)m = ((F (u))(Θ,θ) ,
(Θ,θ) (V,v)
(f (u)) ).
(V,v)
Continuing the proof of Proposition 2, since O(s, t)(Θ,θ) is nonempty or
(Θ,θ) (V,v) (Θ,θ) (V,v) (Θ,θ) (V,v) (V,v)
A(s, t) is nonempty, F (s) 6= F (t) or f (s)(Θ,θ) 6=
(Θ,θ) (V,v) m m
f (t) . Hence, by lemma 13, (s) 6= (t) . Thus, there exists a pure double
Boolean algebra D and a valuation m based on D such that (s)m 6= (t)m . This
ends the proof of Proposition 2.
Hence, O(·, ·) and A(·, ·) are reductions from the WP in pure double Boolean
algebras to the satisfiability problem for K2 . Thus, by Theorem 3,
Corollary 2. The WP in pure double Boolean algebras is in PSPACE.
8 Conclusion
Our results implicitly assume that the set V ar of all individual variables is infi-
nite and the depth of nesting of the left operations with the right operations is
not bounded. Following the line of reasoning suggested in [4], we may see what
happens if we assume that the set V ar of all individual variables is finite and
the depth of nesting of the left operations with the right operations is bounded.
Do we get a linear time complexity in this case?
The unification problem is quite different from the WP discussed here: given
terms s, t, decide whether there exists terms which can be substituted for the
variables in s, t so that the terms thus obtained are identically interpreted in all
pure double Boolean algebras. In Mathematics and Computer Science, unifica-
tion problems are of the utmost importance. At the time of writing, we know
nothing about the decidability/complexity of the unification problem in pure
double Boolean algebras.
Acknowledgements
Special acknowledgement is heartly granted to Christian Herrmann who made
several helpful comments for improving the correctness and the readability of
this article.
References
1. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press
(2001).
2. Davey, B, Priestley, H.: Introduction to Lattices and Order. Cambridge University
Press (2002).
3. Ganter, B, Wille, R.: Formal Concept Analysis: Mathematical Foundations. Springer
(1999).
4. Halpern, J.: The effect of bounding the number of primitive propositions and the
depth of nesting on the complexity of modal logic. Artificial Intelligence 75 (1995)
361–372.
5. Herrmann, C., Luksch, P., Skorsky, M., Wille, R.: Algebras of semiconcepts and
double Boolean algebras. Technische Universität Darmstadt (2000).
6. Vormbrock, B.: A first step towards protoconcept exploration. In Eklund, P. (editor):
Concept Lattices. Springer (2004) 208–221.
7. Vormbrock, B.: Complete subalgebras of semiconcept algebras and protoconcept alge-
bras. In Ganter, B., Godin, R. (editors): Formal Concept Analysis. Springer (2005)
329–343.
8. Vormbrock, B.: A solution of the word problem for free double Boolean algebras.
In Kuznetsov, S., Schmidt, S. (editors): Formal Concept Analysis. Springer (2007)
240–270.
9. Vormbrock, B., Wille, R.: Semiconcept and protoconcept algebras: the basic theorems.
In Ganter, B., Stumme, G., Wille, R. (editors): Formal Concept Analysis. Springer
(2005) 34–48.
10. Wille, R.: Restructuring lattice theory: an approach based on hierarchies of con-
cepts. In Rival, I. (editor): Ordered Sets. D. Reidel (1982) 314–339
11. Wille, R.: Boolean concept logic. In Ganter, B., Mineau, G. (editors): Conceptual
Structures: Logical, Linguistic, and Computational Issues. Springer (2000) 317–331.
12. Wille, R.: Formal concept analysis as applied lattice theory. In Ben Yahia, S., Me-
phu Nguifo, E., Belohlavek, R. (editors): Concept Lattices and their Applications.
Springer (2008) 42–67
Annex
Proof of Lemma 10. By induction on A and a.
Basis. Remind that V ar(α) ⊆ {P1 , . . . , Pn }. In this respect, for all positive
integers i, if i ≤ n then (T (Pi ))m = (xi )m = m(xi ) = (V (Pi ), V (Pi ). ) =
.
((Pi )(V,v) , (Pi )(V,v) ).
Hypothesis. Suppose A, B are nice object formulas such that A, B α,
. .
(T (A))m = ((A)(V,v) , (A)(V,v) ) and (T (B))m = ((B)(V,v) , (B)(V,v) ) and a, b
/
are nice attribute formulas such that a, b α, (t(a))m = ((a)(V,v) , (a)(V,v) ) and
/
(t(b))m = ((b)(V,v) , (b)(V,v) ).
Step. We only consider the case of the nice object formula 2a, the other
cases being treated similarly. We have: (T (2a))m = (−l −l −r −r t(a))m =
/ /
¬l ¬l ¬r ¬r (t(a))m = ¬l ¬l ¬r ¬r ((a)(V,v) , (a)(V,v) ) = ¬l ¬l (((a)(V,v) ) , (a)(V,v) ) =
/ /. .
(((a)(V,v) ) , ((a)(V,v) ) ) = ((2a)(V,v) , (2a)(V,v) ).
Proof of Lemma 11. By induction on A and a.
Basis. Remind that V ar(α) ⊆ {P1 , . . . , Pn }. In this respect, for all positive in-
tegers i, if i ≤ n then (Pi )(V,v) = V (Pi ) = Fm(xi ) = F(xi )m = F(T (Pi ))m .
Hypothesis. Suppose A, B are nice object formulas such that A, B α, (A)(V,v)
= F(T (A))m and (B)(V,v) = F(T (B))m and a, b are nice attribute formulas such
that a, b α, (a)(V,v) = I(t(a))m and (b)(V,v) = I(t(b))m .
Step. We only consider the case of the nice object formula 2a, the other cases
being treated similarly. We have: (2a)(V,v) = {F ∈ Fp (D): for all I ∈ Ip (D),
if I ∈ (a)(V,v) then F ∆ I} = {F ∈ Fp (D): for all I ∈ Ip (D), if I ∈ I(t(a))m
then F ∆ I} = I(t(a))m / = F¬r ¬r (t(a))m = F¬l ¬l ¬r ¬r (t(a))m = F(−l −l −r −r t(a))m
= F(T (2a))m .
Proof of Lemma 12. By induction on u.
Basis. Remind that V ar(s) ∪ V ar(t) ⊆ {x1 , . . . , xn }. In this respect, for all pos-
(V,v) (V,v)
itive integers i, if i ≤ n then (F (xi ))(Θ,θ) = (Pi )(Θ,θ) = Fm(xi ) = F(xi )m
(Θ,θ) (V,v) (Θ,θ) (V,v)
and (f (xi )) = (pi ) = Im(xi ) = I(xi )m .
Hypothesis. Suppose u, v are terms such that u s or u t, v s or v t,
(V,v) (V,v) (V,v)
(F (u))(Θ,θ) = F(u)m , (f (u))(Θ,θ) = I(u)m , (F (v))(Θ,θ) = F(v)m and
(V,v)
(f (v))(Θ,θ) = I(v)m .
Step. We only consider the case of the term u ul v, the other cases being treated
(V,v) (V,v)
similarly. We have: (F (u ul v))(Θ,θ) = (F (u) ∧ F (v))(Θ,θ) = ((F (u))(Θ,θ)
(V,v) (V,v)
∧(F (v))(Θ,θ) )(V,v) = (F (u))(Θ,θ) ∩ (F (v))(Θ,θ) = F(u)m ∩ F(v)m =
(Θ,θ) (V,v) (V,v)
F(u)m ∧l (v)m = F(uul v)m and (f (u ul v)) = (2(F (u) ∧ F (v)))(Θ,θ) =
.
(2((F (u))(Θ,θ) ∧ (F (v))(Θ,θ) ))(V,v) = ((F (u))(Θ,θ) ∧ (F (v))(Θ,θ) )(V,v) =
(V,v) (V,v) .
((F (u))(Θ,θ) ∩(F (v))(Θ,θ) ) = (F(u)m ∩F(v)m ). = I(u)m ∧l (v)m = I(uul v)m .
Proof of Lemma 13. By induction on u.
Basis. Remind that V ar(s) ∪ V ar(t) ⊆ {x1 , . . . , xn }. In this respect, for all
positive integers i, if i ≤ n then (xi )m = m(xi ) = ((Θ(Pi ))(V,v) , (θ(pi ))(V,v) ) =
(V,v) (V,v) (V,v) (V,v)
((Pi )(Θ,θ) , (pi )(Θ,θ) ) = ((F (xi ))(Θ,θ) , (f (xi ))(Θ,θ) ).
Hypothesis. Suppose u, v are terms such that u s or u t, v s or
(V,v) (V,v) (V,v)
v t, (u)m = ((F (u))(Θ,θ) , (f (u))(Θ,θ) ) and (v)m = ((F (v))(Θ,θ) ,
(V,v)
(f (v))(Θ,θ) ).
Step. We only consider the case of the term u ul v, the other cases being treated
(V,v) (V,v)
similarly. We have: (u ul v)m = (u)m ∧l (v)m = ((F (u))(Θ,θ) , (f (u))(Θ,θ) )
(V,v) (V,v) (V,v) (V,v)
∧l ((F (v))(Θ,θ) , (f (v))(Θ,θ) ) = ((F (u))(Θ,θ) ∩ (F (v))(Θ,θ) ,
(V,v) (V,v) .
((F (u))(Θ,θ) ∩ (F (v))(Θ,θ) ) ) = (((F (u))(Θ,θ) ∧ (F (v))(Θ,θ) )(V,v) ,
. (V,v)
((F (u))(Θ,θ) ∧ (F (v))(Θ,θ) )(V,v) ) = ((F (u) ∧ (F (v))(Θ,θ) , (2((F (u))(Θ,θ) ∧
(Θ,θ) (V,v) (V,v)
(F (v))(Θ,θ) ))(V,v) ) = ((F (u ul v)) , (2(F (u) ∧ F (v)))(Θ,θ) ) =
(Θ,θ) (V,v) (Θ,θ) (V,v)
((F (u ul v)) , (f (u ul v)) ).