The aim of this article is to prove that the word problem in semiconcept algebras is PSPACE-complete.
In formal concept analysis [
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 equational 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 [
Sections 2 and 3 show some of the basic properties of formal contexts and semiconcept 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
In formal concept analysis, the properties of semiconcepts are re ected 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".
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. = fm 2 M : for all g 2 G, if g 2 X then g Y / = fg 2 G: for all m 2 M , if m 2 Y then g mg mg 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, fo1g. = fa1; a2g and fa2g/ = fo1g.
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 / i 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 ,
X2 then X1. X2.,
Y2 then Y1/ Y2/, X./ and X. = X./.,
Y and Y / = Y /./. 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 n X; (G n 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 nite then Hl(IK) is nite too and moreover, j Hl(IK) j = 2jGj. 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 n , [ and \ on 2G. Hence, Hl(IK) satis es 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 n Y )/; M n 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 nite then Hr(IK) is nite too and moreover, j Hr(IK) j = 2jMj. 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 n , [ and \ on 2M . Hence, Hr(IK) satis es 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" i 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 (;; fa1; a2g), (fo1g; fa1; a2g), (fo2g; fa1g), (fo1g; fa2g), (fo1; o2g; fa1g) and (fo1; o2g; ;). 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 n X; (G n X).), :r(X; Y ) = ((M n Y )/; M n 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 = (;; fa1; a2g), >l = (fo1; o2g; fa1g), ?r = (fo1g; fa1; a2g) and >r = (fo1; o2g; ;).
Remark that if G; M are nite then H(IK) is nite too and moreover, j H(IK) j 2jGj + 2jMj. 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 n , [ 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 n , [ and \ on 2M . In other respects, it is a simple matter to check that H(IK) satis es the following conditions for every x; y; z 2 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) = :lx and :r(x _r x) = :rx, { 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(:lx ^l :ly) = x _l y and :r(:rx _r :ry) = 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 :lx = ?l and x _r :rx = >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 rst 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 de ned by (X1; Y1) v (X2; Y2) i X1
X2 and Y1
Y2 for every (X1; Y1); (X2; Y2) 2 H(IK). Obviously, for all (X1; Y1); (X2; Y2) 2 H(IK), { (X1; Y1) v (X2; Y2) i (X1; Y1)^l (X2; Y2) = (X1; Y1)^l (X1; Y1) and (X1; Y1) _r(X2; Y2) = (X2; Y2) _r (X2; Y2), { if (X1; Y1) 2 Hl(IK) then (X1; Y1) v (X2; Y2) i (X1; Y1) ^l (X2; Y2) = (X1; Y1), { if (X2; Y2) 2 Hr(IK) then (X1; Y1) v (X2; Y2) i (X1; Y1) _r (X2; Y2) = (X2; Y2).
Moreover, the binary relation v is re exive, 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 i the operations ?l, ?r, >l, >r, :l, :r, _l, _r, ^l and ^r satisfy the 15 above conditions.
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 bra. We de ne Let D = (D; ?l; ?r; >l; >r; :l; :r; _l; _r; ^l; ^r) be a pure double Boolean algeDl = fx ^l x: x 2 Dg
Dr = fx _r x: x 2 Dg 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 Obviously, the operations ?l, >l, :l, _l and ^l are stable on Dl and the operations ?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 structures of type (0; 0; 1; 2; 2). More precisely, they are Boolean algebras. Moreover, the set D can be ordered by the binary relation de ned by x
y i x ^l y = x ^l x and x _r y = y _r y for every x; y 2 D. Obviously, for all x; y 2 D, { if x 2 Dl then x { if y 2 Dr then x y i x ^l y = x, y i x _r y = y.
Moreover, the binary relation
is re exive, antisymmetric and transitive on D. q
q (fo1; o2g; ;)
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 lter i for all x; y 2 D, { x; y 2 F implies x ^l y 2 F , { x 2 F and x y imply y 2 F . { x; y 2 I implies x _r y 2 I, { x 2 I and y x imply y 2 I.
A nonempty subset I of D is called an ideal i for all x; y 2 D, The following lemma explains how lters and ideals can be transformed into lters and ideals of the Boolean algebras Dl and Dr.
Lemma 1. Let F; I be nonempty subsets of D. If F is a lter then F \ Dl is a lter of the Boolean algebra Dl and F \ Dr is a lter 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 de ne [F ) = fx 2 D: there exists y 2 F such that y (I] = fx 2 D: there exists y 2 I such that x xg yg The following lemma explains how lters of the Boolean algebra Dl and ideals of the Boolean algebra Dr can be transformed into lters and ideals. Lemma 2. Let F be a nonempty subset of Dl, I be a nonempty subset of Dr. If F is a lter of the Boolean algebra Dl then [F ) is a lter 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 lters F such that F \Dl is a prime lter 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 i 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 lters F for which F \ Dl is a prime lter 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 i F \ I is nonempty. Let
H(IK(D)) = (H(IK(D)); ?0l; ?0r; >0l; >0r; :0l; :0r; _0l; _0r; ^0l; ^0r)
Fx = fF 2 Fp(D): x 2 F g
Ix = fI 2 Ip(D): x 2 Ig Here, the rst results are Lemma 4. Let x 2 D. Fx^lx = Fx and Ix_rx = Ix.
Lemma 5. Let x 2 D. If x 2 Dl then Fx. = Ix and if x 2 Dr then Ix/ = Fx. Lemma 6. Let x 2 D. F:.l:lx = I:l:lx and I:/r:rx = F:r:rx. 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 2 D. The pair (Fx; Ix) is a semiconcept of IK(D). Lemma 8. Let x; y 2 D. If x 6= y then (Fx; Ix) 6= (Fy; Iy).
For all x 2 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 2 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:lx = Fp(D) n Fx and I:lx = (Fp(D) n Fx)., { F:rx = (Ip(D) n Ix)/ and I:rx = Ip(D) n Ix, { Fx_ly = Fx [ Fy and Ix_ly = (Fx [ Fy)., { Fx_ry = (Ix \ Iy)/ and Ix_ry = Ix \ Iy, { Fx^ly = Fx \ Fy and Ix^ly = (Fx \ Fy)., { Fx^ry = (Ix [ Iy)/ and Ix^ry = Ix [ Iy. Theorem 1. The function h is a homomorphism from D to H(IK). In other words: every pure double Boolean algebra is concrete.
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 j 0l j 0r j 1l j 1r j ls j rs j (s tl t) j (s tr t) j (s ul t) j (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 algebra. 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 de ned below is a valuation based on the pure double Boolean algebra D2;2 de ned in Example 5: m2;2(x) = (fo2g; fa1g), m2;2(y) = (fo1g; fa2g) and for all individual variables z, if z 6= x; y then m2;2(z) = (fo1; o2g; fa1g). 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, ( ls)m = :l(s)m, ( rs)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. y)m2;2 = (fo1; o2g; ;) and ( lx)m2;2 = (fo1g; fa1; a2g).
Example 9. Concerning the valuation m2;2 de ned in Example 8, we have (x tr 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 rst, 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 satis ability problem of numerous modal logics [1, Chapter 6]. Therefore, we introduce in Section 5 a PSPACEcomplete modal logic and we show in Sections 6 and 7 how to reduce one into the other its satis ability problem and the WP in pure double Boolean algebras.
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 j ? j :A j (A _ B) j 2a
a ::= p j ? j :a j (a _ b) j 2A The other Boolean constructs are de ned 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 i 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 i { V ar( )
OV ar or V ar( ) Let IK = (G; M; ) be a formal context. A IK-valuation is a pair (V; v) of functions 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 n (A)(V;v), (A _ B)(V;v) = (A)(V;v) [ (B)(V;v), (2a)(V;v) = fg 2 G: for all m 2 M , if m 2 (a)(V;v) then g mg, (p)(V;v) = v(p), (?)(V;v) = ;, (:a)(V;v) = M n (a)(V;v), (a _ b)(V;v) = (a)(V;v) [ (b)(V;v) and (2A)(V;v) = fm 2 M : for all g 2 G, if g 2 (A)(V;v) then g mg. 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 satis able i { there exists a formal context IK = (G; M; ) and a IK-valuation (V; v) such that ( )(V;v) is nonempty. 5.3
Decision
input: a nice formula , output: determine whether
is satis able.
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 satis ability problem for K2 is PSPACE-hard. Proof. A reduction similar to the reduction from the QBF -validity problem to the satis ability problem for K considered in [1, Theorem 6.50] can be easily obtained.
input: a formula , output: determine whether
is satis able.
Theorem 3. The satis ability 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 satis ability problem for K2 and the satis ability problem for K2 are both PSPACE-complete.
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 satis able i 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) = lT (A), T (A _ B) = T (A) tl T (B), T (2a) = l l r r t(a), t(pi) = yi, t(?) = 1r, t(:a) = rt(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 j j. Moreover, Proposition 1. If is nice then is satis able i 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( ) fP1; : : : ; Png. ()) Suppose is satis able, 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 satis able, 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 rst 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 satis able. 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 satis able. This ends the proof of Proposition 1.
Hence, (s1( ); s2( )) is a reduction from the nice satis ability 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
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 i some instance of O(s; t) is satis able or some instance of A(s; t) is satis able. 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 ( ls) = :F (s), f ( ls) = 2:F (s), F ( rs) = 2:f (s), f ( rs) = :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 (sult) = F (s)^F (t), f (sult) = 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 j (s; t) j. 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 i there exists a substitution ( ; ) such that ( ; ) is normal with respect to OV ar and AV ar and O(s; t)( ; ) is satis able or A(s; t)( ; ) is satis able.
Proof. Let n be a positive integer such that V ar(s) [ V ar(t) fx1; : : : ; xng. ()) 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 substitution ( ; ) such that ( ; ) is normal with respect to OV ar and AV ar and O(s; t)( ; ) is satis able or A(s; t)( ; ) is satis able. Let ( ; ) be a normal substitution 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, if i
n then if m(xi) is in Dl then (Pi)( ; )(V;v) = (Pi)(V;v) = V (Pi) = Fm(xi) and if m(xi) is in Dr then (Pi)( ; )(V;v) = (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 Dl then (pi)( ; )(V;v) = (2Pi)(V;v) = (Pi)(V;v). = V (Pi). = F m.(xi) = Im(xi) and if m(xi) is in Dr then (pi)( ; )(V;v) = (pi)(V;v) = v(pi) = Im(xi) We rst observe
s or u and (f (u))( ; )(V;v) = 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 6= I(t)m . Hence, by Lemma 12, O(s; t)( ; )(V;v) is nonempty or A(s; t)( ; )(V;v) is nonempty. Thus, there exists a substitution ( ; ) such that ( ; ) is normal with respect to OV ar and AV ar and O(s; t)( ; ) is satis able or A(s; t)( ; ) is satis able. (() Suppose there exists a substitution ( ; ) such that ( ; ) is normal with respect to OV ar and AV ar and O(s; t)( ; ) is satis able or A(s; t)( ; ) is satis able, 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 satis able or A(s; t)( ; ) is satis able, there exists a formal context IK = (G; M; ) and a valuation (V; v) based on IK such that O(s; t)( ; )(V;v) is nonempty or A(s; t)( ; )(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) = (( (Pi))(V;v); ( (pi))(V;v)). Interestingly, t then (F (u))( ; )(V;v) = F(u)m
(f (u))( ; )(V;v)).
s or u t then (u)m = ((F (u))( ; )(V;v); Continuing the proof of Proposition 2, since O(s; t)( ; )(V;v) is nonempty or A(s; t)( ; )(V;v) is nonempty, F (s)( ; )(V;v) 6= F (t)( ; )(V;v) or f (s)( ; )(V;v) 6= f (t)( ; )(V;v). Hence, by lemma 13, (s)m 6= (t)m. 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 satis ability problem for K2. Thus, by Theorem 3, Corollary 2. The WP in pure double Boolean algebras is in PSPACE. 8
Our results implicitly assume that the set V ar of all individual variables is in
nite and the depth of nesting of the left operations with the right operations is
not bounded. Following the line of reasoning suggested in [
Special acknowledgement is heartly granted to Christian Herrmann who made several helpful comments for improving the correctness and the readability of this article.
Basis. Remind that V ar( ) fP1; : : : ; Png. 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(:al):(Vr;:v)r)(/t;((a()a))m(V;=v)):/.l:)l=:r(:(2r(a(a)()V(V;v;)v;)(/2;(aa))((VV;;vv)).)).= :l:l(((a)(V;v))/; (a)(V;v)) =
Basis. Remind that V ar( ) fP1; : : : ; Png. In this respect, for all positive integers 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) = fF 2 Fp(D): for all I 2 Ip(D), if I 2 (a)(V;v) then F Ig = fF 2 Fp(D): for all I 2 Ip(D), if I 2 I(t(a))m then F
Ig = I(t(a))m / = F:r:r(t(a))m = F:l:l:r:r(t(a))m = F( l l r rt(a))m = F(T (2a))m .
Proof of Lemma 12. By induction on u.
Basis. Remind that V ar(s) [ V ar(t) fx1; : : : ; xng. In this respect, for all positive integers i, if i n then (F (xi))( ; )(V;v) = (Pi)( ; )(V;v) = Fm(xi) = F(xi)m and (f (xi))( ; )(V;v) = (pi)( ; )(V;v) = Im(xi) = I(xi)m .
Hypothesis. Suppose u; v are terms such that u s or u t, v s or v t, (F (u))( ; )(V;v) = F(u)m , (f (u))( ; )(V;v) = I(u)m , (F (v))( ; )(V;v) = F(v)m and (f (v))( ; )(V;v) = I(v)m .
Step. We only consider the case of the term u ul v, the other cases being treated similarly. We have: (F (u ul v))( ; )(V;v) = (F (u) ^ F (v))( ; )(V;v) = ((F (u))( ; ) ^(F (v))( ; ))(V;v) = (F (u))( ; )(V;v) \ (F (v))( ; )(V;v) = F(u)m \ F(v)m = F(u)m^l(v)m = F(uulv)m and (f (u ul v))( ; )(V;v) = (2(F (u) ^ F (v)))( ; )(V;v) = (2((F (u))( ; ) ^ (F (v))( ; )))(V;v) = ((F (u))( ; ) ^ (F (v))( ; ))(V;v). = ((F (u))( ; )(V;v)\(F (v))( ; )(V;v)). = (F(u)m \F(v)m ). = I(u)m^l(v)m = I(uulv)m . Proof of Lemma 13. By induction on u.
Basis. Remind that V ar(s) [ V ar(t) fx1; : : : ; xng. In this respect, for all = (((F (u))( ; ) ^ (F (v))( ; ))(V;v); ((F (u))( ; ) ^ (F (v))( ; ))(V;v).) = ((F (u) ^ (F (v))( ; )(V;v); (2((F (u))( ; ) (F (v))( ; )))(V;v)) = ((F (u ul v))( ; )(V;v); (2(F (u) ^ F (v)))( ; )(V;v)) =^ ((F (u ul v))( ; )(V;v); (f (u ul v))( ; )(V;v)).