Dual tableau-based decision procedures for some relational logics⋆

Abstract

We consider fragments of the relational logic RL(1) obtained by imposing some constraints on the relational terms involving relations composition. Such fragments allow to express several non classical logics such as the multi-modal logic K and the description logic ALC with union and intersection of roles. We show how relational dual tableaux can be employed to define decision procedures for each of them.

Introduction

2 2.1

Syntax propositional connectives of disjunction, conjunction, and negation may be interpreted as union, intersection, and complement of relations, respectively. In modal (resp., description) logics, a possibility operator hRi (resp., a concept operator ∃R) determined by a relation (resp., role) R acting on a formula α, interpreted as a right ideal relation, may be understood as R ; α, as observed in [11]. It is known that the composition of a relation with a right ideal relation returns a right ideal relation. The relational interpretation of languages preserves validity of formulae. In [7] an implementation of the translation of modal languages into relational languages is presented.

Relational logics appear to be an adequate representation means for a great variety of theories as shown in [12]. Therefore any decision procedure for a relational logic is not just a single decision method for some theory but it may be applied to several theories which can be interpreted in this relational logic.

The paper is organized as follows. In Section 2 we recall the logic RL( 1 ) and its dual tableau. In Sections 3 and 4 we present two fragments of RL( 1 ) and we develop decision procedures for them based on dual tableaux.

The relational logic RL( 1 ) and its dual tableau Let OV be a countably infinite set of object (individual) variables x, y, z, w . . ., let RV be a countably infinite set of relational variables p, q, r, s, . . ., and let 1 be the relational constant. The relational operators are − (complementation), ∩ (intersection), ∪ (union), ; (composition), and −1 (converse). The set of relational terms RT is the smallest set (with respect to inclusion) such that (a) RV ⊆ RT, (b) 1 ∈ RT, and (c) RT is closed with respect to the relational operators.

Relational terms are indicated with the letters P , Q, R,... Examples of relational terms are (p ∩ q) ; s and −(P ∪ Q), where p, q, and s are relational variables and P, Q are relational terms. RL( 1 )-formulae have the form xRy, where x, y ∈ OV and R ∈ RT. The RL( 1 )-formulae x1y and xry, with r ∈ RV, are called atomic RL( 1 )-formulae. A literal is an atomic formula (x1y or xry) or its complementation (x(−1)y or x(−r)y). RL( 1 )-formulae are also denoted using as metavariables the greek letters ϕ and ψ. For a relational operation ♯, by a (♯)-formula we mean a formula built with a relational term whose principal operation is ♯ whereas by a (−♯)-formula we denote a formula obtained from a relational term with principal operation − followed by ♯. A Boolean term is a relational term such that all the relational operations in it are among the Boolean operations −, ∪, and ∩. 2.2

Semantics RL( 1 )-formulae are interpreted in RL( 1 )-models. An RL( 1 )-model is a structure M = (U, m), where U is a nonempty universe and m : RV → U × U is a given map which is naturally extended to the whole collection RT of relational terms as follows: – m( 1 ) = U × U ; – m(−R) = (U × U ) \ m(R); – m(R ∪ S) = m(R) ∪ m(S); – m(R ∩ S) = m(R) ∩ m(S); – m(R ; S) = m(R) ; m(S)

= {(x, y) ∈ U ×U : (x, z) ∈ m(R) and (z, y) ∈ m(S), for some z ∈ U }; – m(R−1) = {(y, x) ∈ U × U : (x, y) ∈ m(R)}.

Let M = (U, m) be an RL( 1 )-model. An evaluation in M is any function v : OV → U . Given an object variable z in OV, an evaluation v1 is a z-variant of an evaluation v if v1(x) = v(x), for every x ∈ OV such that x 6= z. Satisfaction of an RL( 1 )-formula xRy by an RL( 1 )-model M = (U, m) and by an evaluation v in M is defined as:

M, v |= xRy iff (v(x), v(y)) ∈ m(R).

An RL( 1 )-formula xRy is true in a model M = (U, m) if M, v |= xRy, for every evaluation v in M. An RL( 1 )-formula xRy is said valid if it is true in all RL( 1 )models. An RL( 1 )-formula xRy is falsified by a model M = (U, m) and by an evaluation v in M if M, v 6|= xRy. It is falsifiable if there are a model M and an evaluation v in M such that M, v 6|= xRy. 2.3

RL(1)-dual tableau

Proof development in dual tableaux proceeds by systematically decomposing the (disjunction of) formula(e) to be proved till a validity condition is detected by means of axiomatic sets. Such an analytic approach is similar to the one adopted by the tableau method with the difference that the two systems work in a dual way. Duality of tableaux and of dual tableaux has been deeply analyzed in [9].

RL( 1 )-dual tableau consists of decomposition rules to analyze the structure of the formula to be proved valid, and of axiomatic sets which specify the closure conditions. The decomposition rules for RL( 1 ) are illustrated in Table 1. In these rules, “,” is interpreted as disjunction and “|” as conjunction.

RL( 1 )-axiomatic sets are sets of RL( 1 )-formulae including a subset of one of the following forms: (Ax 1) {xRy, x(−R)y}, (Ax 2) {x1y}.

Let xP y be an RL( 1 )-formula. An RL( 1 )-proof tree for xP y is an ordered tree whose nodes are labelled by disjunctive sets of formulae. By a branch of a proof tree we mean any maximal path in it. We require a proof tree for xP y to satisfy the following properties: – the formula xP y is at the root of this tree, – each node, with the exception of the root, is obtained from its predecessor node by an application of a decomposition rule of Table 1, – a node does not have successors (i.e. it is a leaf node) whenever its set of formulae is an axiomatic set or none of the rules of Table 1 can be applied to its set of formulae.

A node of an RL( 1 )-proof tree is closed if its associated set of formulae contains an axiomatic set. A branch is closed if one of its nodes is closed. A proof tree is closed if all of its branches are closed. An RL( 1 )-formula is provable if there is a closed RL( 1 )-proof tree for it, referred to as an RL( 1 )-proof.

A node of an RL( 1 )-proof tree is falsified by a model M = (U, m) and by an evaluation v if every formula xRy in its set of formulae is falsified by M and v. A node is falsifiable if there are a model M and an evaluation v such that it is falsified by M and v. A branch of an RL( 1 )-proof tree is falsified by a model M and by an evaluation v if each node in it is falsified by M and v. A branch of an RL( 1 )-proof tree is falsifiable if there is a model and an evaluation which falsify every node in the branch. An RL( 1 )-proof tree is falsified by a model M = (U, m) and by an evaluation v if one of its branches is falsified by M and v. Finally, an RL( 1 )-proof tree is falsifiable if one of its branches is falsifiable.

Correctness and completeness of RL( 1 )-dual tableau are proved in [12]. The logic RL( 1 ) is undecidable. Such result follows from the undecidability of the equational theory of representable relation algebras discussed in [16]. In the following sections we present some of its decidable fragments. Other decidable fragments of RL( 1 ) can be found in [12]. 3

The (r ; )-fragment of RL( 1 ) and its decision procedure The (r ; )-fragment is the collection of the RL( 1 )-formulae xP y in which the composition operator “ ; ” can occur only in the following restricted way. For each subterm of P of the form R ; S, R must belong to a designated nonempty proper subset of RV, RV1, whereas S can involve all the relational operators used to construct RL( 1 )-formulae, with the exception of the converse operator −1. In the relation interpretation of logics, the elements of RV1 are meant to denote accessibility relations (resp., roles) in modal (resp., description) logics.

A formal description of the set of relational terms RT(r ; ) is given in what follows.

Let RV1 be as above, then we define the set of terms RT(r ; )1 as the smallest set of terms containing RV1 which is closed with respect to the complementation operator “−”.

Likewise, we define RT(r ; )2 as the smallest set of terms containing the constant 1 and the relational variables in RV\ RV1, and such that if R, S ∈ RT(r ; )2 and r ∈ RV1, then −R, R ∪ S, R ∩ S, r ; S ∈ RT(r ; )2 . Finally we put

RT(r ; ) =Def RT(r ; )1 ∪ RT(r ; )2 .

This logic allows to express the multi-modal logic K and, therefore, also the description logic ALC [2, 1]. The translation of such logics in relational terms is carried out along the lines of [12], Chapter 7. In particular, the relational variables in RV1 represent the accessibility relations of the multi-modal logic K and the roles of the logic ALC. A relational dual tableau style decision procedure for the logic K can be found in [8]. The procedure defined there is inspired by [3]. 3.1

A dual tableau decision procedure for the (r ; )-fragment Dual tableaux for the (r ; )-fragment can be obtained by adapting the system introduced in Section 2.3 as we describe below.

Axiomatic sets are defined as in Section 2.3. The set of decomposition rules for the Boolean operators, namely the (∪), (∩), (−∩), (−∪), (−−)-rules, are identical to the ones presented in Table 1. The other decomposition rules, that is the ( ; )-rule and the (− ; )-rule, are displayed in Table 2.3 The notion of proof tree is identical to the one given in Section 2.3 with the exception that each node can be obtained from its predecessor (if any) by the application of a Boolean decomposition rule of Table 1 or a decomposition rule of Table 2. In particular, the ( ; )-rule of Table 2 can be applied to a formula x(r ; S)y of a node of a proof tree only in case the literal x(−r)z occurs in the same node. Such side condition makes this variant of the ( ; )-rule less liberal than the corresponding 3 Table 2 does not contain any decomposition rule for the converse operation −1 because it is not a constructor of the terms belonging to the (r ; )-fragment. rule presented in Table 1, since it restricts the choice of the variable which can be used in the decomposition step. Moreover, such a rule variant does not perform any branch splitting and therefore the overall number of branches in the proof tree is generally smaller.

A proof procedure for the dual tableau system just defined, that we call (r ; )-dual tableau, can be designed by giving a description of the proof tree construction process together with the constraints which limit the application of the decomposition rules.

For this purpose, we introduce the notion of deduction tree. As proof trees, deduction trees are ordered trees whose nodes are labelled with disjunctive sets. However, deduction trees may have some leaf nodes that do not contain any axiomatic set and such that decomposition rules can still be applied to them. As it is clarified below, deduction trees can be seen as “approximations” of proof trees with the property that they can be completed to proof trees. Definition 1. Let xP y be a formula of the (r ; )-fragment of RL( 1 ). A deduction tree T for xP y is recursively defined as follows: (a) the tree with only one node labelled with {xP y} is a deduction tree for xP y (initial deduction tree); (b) let T be a deduction tree for xP y and let θ be a branch of T whose leaf node N does not contain an axiomatic set.4 The tree obtained from T by applying one of the Boolean decomposition rules of Table 1 or one of the decomposition rules of Table 2, as illustrated by items 1-5 below, is a deduction tree for xP y: 1. if any formula of type x(R ∪ S)y (resp., x(−(R ∩ S))y) occurs in N , we add N ′ = (N \ {x(R ∪ S)y}) ∪ {xRy, xSy} (resp., N ′ = (N \ {x(−(R ∩ Sy))}) ∪ {x(−R)y, x(−S)y}) as the successor of N in θ; 2. if any formula of type x(R ∩ S)y (resp., x(−(R ∪ S))y) occurs in N , we simultaneously add N ′ = (N \ {x(R ∩ S)y}) ∪ {xRy} (resp., N ′ = (N \ {x(−(R ∪ S))y}) ∪ {x(−R)y}) as left successor of N , and N ′′ = (N \{x(R∩S)y})∪{xSy} (resp., N ′′ = (N \{x(−(R∪S))y})∪{x(−S)y}) as right successor of N in θ; 3. if any formula of type x(− − R)y occurs in N , we add N ′ = (N \ {x(− −

R)y}) ∪ {xRy} as the successor of N in θ; 4. if any formula of type x(−(r ; S))y occurs in N , we add N ′ = (N \ {x(−(r ; S))y}) ∪ {x(−r)z, z(−S)y} as the successor of N in θ; 5. if any formula of type x(r ; S)y occurs in N and a literal x(−r)z occurs in N we add N ′ = N ∪ {zSy} as the successor of N in θ.

We further require that the following strictness hypotheses are satisfied: on each branch of a deduction tree – all the decomposition rules, with the exception of the ( ; )-rule, can be applied at most once to the same non-literal formula, – the ( ; )-rule can be applied at most once with the same premises. 4 From now on we identify nodes with the (disjunctive) sets labelling them. It is easy to see that if all the branches of a deduction tree T are either closed or, according to the strictness hypotheses, not further expansible, then T is a proof tree. The proof construction in Definition 1 is sound and complete even under the above strictness hypotheses. We will limit ourselves in showing only its termination, thus obtaining a decision procedure for the (r ; )-fragment. 3.2 The proof procedure presented in Section 3.1 adds to the current deduction tree one or two new nodes at each decomposition step. Thus, in order to show that it always terminates, it is enough to prove that, given a formula xP y of the (r ; )-fragment, every proof tree for xP y that can be constructed according to the procedure described in Section 3.1 is finite. Before going into details it is useful to introduce the notion of open saturated branch. We characterize an open saturated branch θS of a deduction tree T for a formula xP y of the (r ; )fragment as a set of nodes such that: – x′1y′ ∈/ N , for every node N ∈ θS; – if x′Ry′, (resp., x′(−R)y′) occurs in a node N ∈ θS, then x′(−R)y′ (resp., x′Ry′) does not occur in any other node N ′ ∈ θS; – if x′(− − R)y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that x′Ry′ ∈ N ′; – if x′(R ∩ S)y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that either x′Ry′ ∈ N ′ or x′Sy′ ∈ N ′; – if x′(R ∪ S)y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that x′Ry′ ∈ N ′ and x′Sy′ ∈ N ′; – if x′(−(R ∩ S))y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that x′(−R)y′, x′(−S)y′ ∈ N ′; – if x′(−(R ∪ S))y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that either x′(−R)y′, or x′(−S)y′ ∈ N ′; – if x′(r ; S)y′ occurs in a node N ∈ θS, then for every z such that x′(−r)z ∈ N ′, for some N ′ ∈ θS, there is an N ′′ ∈ θS such that zSy′ ∈ N ′′; – if x′(−(r ; S))y′ occurs in a node N ∈ θS, then there is a node N ′ ∈ θS such that x′(−r)z, z(−S)y′ ∈ N ′, for some object variable z.

The proof can be carried out by contradiction, assuming that one can construct an infinite proof tree for xP y under the strictness hypotheses. By K¨onig’s Lemma, such a proof tree must have an infinite branch. This branch cannot be closed because once a branch is closed, it cannot be further expanded. Thus it can be embedded in an open saturated branch.

We devote the rest of this section to proving that under the strictness hypotheses every open saturated branch of a proof tree for xP y has to be finite. This result is sufficient to assert, in contradiction with our hypothesis, that each branch of a proof tree for a formula xP y has to be finite. Thus, each proof tree for xP y has to be finite and therefore the proof procedure of Section 3.1 always terminates.

To carry out our proof, it is useful to consider that since nodes of a proof tree are finite sets of formulae, a branch containing a finite number of nodes is finite.

Let θS be a saturated branch of a proof tree T for a formula xP y. We define a total order <θS on WθS \ {y} as follows: for z, w ∈ WθS \ {y} we let z <θS w if and only if z has been introduced before w in the construction of the branch θS . Lemma 1. The number of formulae in S θS with left variable w is finite, for every w ∈ WθS .

Proof: The lemma is trivially true for the variable y, since S θS contains no formula with left variable y. Concerning the variables in S θS , we proceed by induction over the ordered set (WθS \ {y}, <θS ).

– Base case. The initial formula xP y can generate, by Boolean decomposition, a finite number of subformulae with left variable x. Moreover, each application of the (− ; )-decomposition rule introduces a literal of type x(−r)z that, however, cannot be further decomposed, and every application of the ( ; )-rule does not increase the number of formulae with left variable x. Thus the number of formulae in S θS with left variable x is finite. – Inductive step. By inductive hypothesis, the number of formulae in S θS with left variable z is finite, for z <θS w. We prove that this holds for w as well.

The variable w has been introduced by the application of the (− ; )-decomposition rule to a formula z(−(r ; S))y. The decomposition of w(−S)y by means of the Boolean rules can introduce in S θS a finite number of subformulae with left variable w. Application of the (− ; )-rule to each of these formulae only adds a literal with left variable w.

Formulae with left variable w can also be obtained by applying the ( ; )decomposition rule to every formula of type z(r ; Q)y (notice that by the (- ; )decomposition of z(−(r ; S))y, the literal z(−r)w occurs in θS ). By inductive hypothesis the number of such z(r ; Q)y has to be finite, thus the number of the wQy formulae resulting from the ( ; )-decomposition is also finite. Finally, applying the Boolean rules and the (− ; )-rule to each of the wQy formulae obtained before, we get a finite number of formulae with left variable w. Summing up, the number of formulae with left variable w is finite.

Let us define recursively the weight of a formula as follows:

– weight (xry) = weight (x(−r)y) = weight (x1y) = 0 follows.

Lemma 2. Any ( ; )-formula in S θS can be decomposed a finite number of Proof: Let z(r ; Q)y be a ( ; )-formula in S θS . Clearly, it can be decomposed as many times as the number of literals z(−r)w in S θS , for any w ∈ WθS . This number is in turn bounded by the number of (− ; )-formulae z(−(r ; P ))y in S θS , for any relational term P . Since by Lemma 1 this number is finite, the lemma ⊔⊓ ⊔⊓ – weight (x(A ∩ P )y) = weight (xAy) + weight (xP y) + 1 – weight (x(−(A ∩ P ))y) = weight (x(−A)y) + weight (x(−P )y) + 1 – weight (x(− − P )y) = weight (P ) + 1 – weight (x(−(r ; P ))y) = weight (z(−P )y) + 1 – weight (x(r ; P )y) = weight (zP y) + 1.

We define the weight of a node N as the sum of the weight s of the formulae in N . In particular, the weight of the ( ; )-formulae that cannot be decomposed anymore in N is set to 0. Analogously we set to 0 the weight s of those non literal formulae in N that are not of type ( ; ) which have been already decomposed in a previous step because they also occur in some ancestors of N . It is easy to check that the weight of a node N is 0 if and only if it contains only literals, ( ; )-formulae that cannot be expanded anymore, and non literal formulae that are not of type ( ; ) already decomposed by some previous inference steps. Lemma 3. Let T0 be an initial deduction tree for xP y. After a finite number of steps a proof tree T can be constructed such that each of its leaf nodes have all weight 0.

Sketch of the proof: Each time a rule (∩), (∪), (−−), or (− ; ) is applied to a formula on a leaf node of a deduction tree, the new nodes have a lower weight. If a decomposition step yields a non literal formula that is not of type ( ; ), that already occurs in some ancestor nodes and that has been decomposed in a previous step, the weight of that formula is set to 0 and by the strictness hypotheses it is not decomposed anymore. Each time a ( ; )-formula is expanded, the weight of the node is incremented. However, by Lemma 2 this may happen only a finite number of times. After that, the ( ; )-formula gets the weight 0 for ever. Notice also that every ( ; )-decomposition introduces a formula of a lower weight. ⊔⊓

Clearly each branch of the proof tree T of Lemma 3 is saturated and finite. Thus every proof tree for xP y, constructed according to the procedure described in Section 3.1, is finite. Hence we can state the following theorem. Theorem 1 (Termination). The dual tableau proof procedure for the (r ; )fragment described in Section 3.1 always terminates. 4

The (∪, ∩ ; )-fragment of RL( 1 ) and its decision procedure The (∪, ∩ ; )-fragment of RL( 1 ) is an extension of the (r ; )-fragment in which the constraints on the composition operator “ ; ” are more relaxed. In particular, the first argument in a term of type R ; S of the (∪, ∩ ; )-fragment can be any term constructed from the relational variables of a proper nonempty subset of RV, say RV1, by applying only the ∪ and ∩ operators. The restriction on the second argument is the same of the (r ; )-fragment: thus S can involve all the relational operators used in RL( 1 )-formulae except the converse operator −1. More precisely, we put

RT(∪,∩ ; ) =Def RT(∪,∩ ; )1 ∪ RT(∪,∩ ; )2 , where RT(∪,∩ ; )1 and RT(∪,∩ ; )1 are defined as follows. RT(∪,∩ ; )1 is the smallest set of terms which contains the relational variables of RV1 and is closed with respect to the operators −, ∪, and ∩, whereas RT(∪,∩ ; )2 is the smallest set of terms involving only the constant 1 and the relational variables RV \ RV1 and such that if P, S ∈ RT(∪,∩ ; )2 and R ∈ PRT(∪,∩ ; )1 , where PRT(∪,∩ ; )1 is the subset of RT(∪,∩ ; )1 whose elements do not contain complemented relational terms, then −P, P ∪ S, P ∩ S, and R ; P ∈ RT(∪,∩ ; )2 .

The (∪, ∩ ; )-fragment of RL( 1 ) can express the description logic ALC(∪, ∩) [2]. Intuitively speaking, formulae of ALC(∪, ∩) can be embedded into the relational framework by mapping role names into the variables in RV1, concept names into the variables in RV \ RV1, and the operator of existential concept restriction “∃”, into the composition operator “ ; ”.

A dual tableau procedure for the (∪, ∩ ; )-fragment

We define a dual tableau system for the (∪, ∩ ; )-fragment of the relational logic RL( 1 ) as follows. Axiomatic sets are defined as in Section 2.3. Concerning the decomposition rules for Boolean formulae and formulae of type (− ; ), we adopt the ones displayed in Table 1.

The ( ; )-rule deserves a separate treatment. We begin by observing that the ( ; )-rule of Table 1 is too liberal in the choice of the object variable to be used in the ( ; )-decomposition and does not allow to define a terminating proof procedure for the (∪, ∩ ; )-fragment. On the other hand the variant of ( ; )-rule of Table 2 turns out to be too restrictive to define a complete system for the (∪, ∩ ; )-fragment.

In order to define a ( ; )-rule that is adequate for our purposes, it is convenient to introduce the following auxiliary notions.

– Let xRy be a Boolean formula of the (∪, ∩ ; )-fragment. We define nnf(xRy) to be the formula obtained from xRy by moving all the occurrences of the complement operator in R as inward as possible. Formally we put nnf(xRy) = x nnt(R)y, where: • if R is an atomic formula or its complementation, then nnt(R) = R; • if R = (S ∩ H), then nnt((S ∩ H)) = (nnt(S) ∩ nnt(H)); • if R = (S ∪ H), then nnt((S ∪ H)) = (nnt(S) ∪ nnt(H)); • if R = (−(S ∩ H)), then nnt((−(S ∩ H))) = nnt((−S)) ∪ nnt((−H)); • if R = (−(S ∪ H)), then nnt((−(S ∪ H))) = nnt((−S)) ∩ nnt((−H)); • if R = (− − S), then nnt((− − S)) = nnt(S).

Clearly xRy and nnf(xRy) are logically equivalent, that is for every model M = (U, m), and every evaluation v, M, v |= xRy if and only if M, v |= nnf(xRy). – Let N be a set of formulae. We characterize the notion of BoolN -formulae as follows: • every literal in N is a BoolN -formula; • every formula of type x(R ∩ S)y is a BoolN -formula if either xRy or xSy is a BoolN -formula; • every formula of type x(R ∪ S)y is a BoolN -formula if both xRy and xSy are BoolN -formulae.

It easy to check that if xSy is a BoolN -formula, then xSy = nnf(xSy). We say that a formula xRy has a Boolean construction from N if there is a BoolN -formula xSy such that xSy = nnf(xRy). – Let R be a Boolean term of RT(∪,∩ ; ), x an object variable, F a set of formulae. Then we define V (R, x, F ) to be the set of object variables z such that xRz has a Boolean construction from F .

Our variant of the ( ; )-rule is formalized as follows:

x(R ; P )y zP y, x(R ; P )y , where: – x(R ; P )y is a formula of the (∪, ∩ ; )-fragment occurring on the leaf node

N of a branch θ of a deduction tree, and – z is an object variable belonging to V (−R, x, S θ).

It is easy to see that V (−R, x, S θ) = V (−R, x, N ) (such identity will be helpful below). Indeed, since N is the leaf node of θ, the set of literals in N is the same as the set of literals in S θ, so that a formula is a BoolN -formula if and only if it is a BoolS θS -formula. Hence, the set of formulae that have a Boolean construction from N is identical to the set of formulae having a Boolean construction from S θ, and the identity V (−R, x, S θ) = V (−R, x, N ) follows.

If x(−R)z is a literal, then V (−R, x, S θ) is the collection of object variables z such that x(−R)z is in N , and therefore, in this case, such variant of the ( ; )-rule coincides with the version presented in Section 3.1.

The ( ; )-rule given above can be obtained from the ( ; )-rule in Table 1 by requiring that the variable z used to decompose x(R ; P )y on the leaf node N of a branch θ can only be selected from the set V (−R, x, S θ) (that is from the set V (−R, x, N )).

In fact, let us assume that we are using the ( ; )-rule of Table 1 to decompose x(R ; P )y: we construct the proof tree by adding as a left successor of N the node N ′ = N ∪ {xRz} and as a right successor of N the node N ′′ = N ∪ {zP y}. Since x(−R)z has a Boolean construction from the literals of N ′ (notice that N ′ contains all the literals in N and recall also that z ∈ V (−R, x, N )), the subproof tree originated from N ′ (which contains xRz) is closed. Consequently we can get rid of the subtree proof originated from N ′ and concentrate on the subtree proof originated from N ′′ only.

Dual tableaux for the (∪, ∩ ; )-fragment are provided with a procedure for constructing proof trees along the lines described in Section 3.1. 4.2

Soundness The proof of soundness of the dual tableaux system for the (∪, ∩ ; )-fragment can be carried out by showing that each step of the construction process of a proof tree for a formula xP y of the (∪, ∩ ; )-fragment preserves falsifiability. Lemma 4. Let T be a falsifiable deduction tree and let T by a step of the proof procedure described in Section 4.1. Then T ′ is a falsifiable ′ be obtained from T deduction tree.

Proof. Since T is falsifiable, there is a branch θ of T that is falsifiable. Let M

= (U, m) and v be respectively a model and an evaluation falsifying each node of θ. If T

′ is obtained from T by expanding a branch different from θ, we are done. Otherwise, suppose that T non-literal formula x′Ex′′ occurring on the leaf node N of θ. The proof that T ′ ′ is obtained from T by decomposing a is falsifiable can be carried out according to the type of the formula x′Ex′′. We consider in detail only the case in which x′Ex′′ is a ( ; )-formula. Thus, suppose that x′Ex′′ = x′(R ; P )x′′ occurs on the leaf node N of a branch θ and that z ∈ V (−R, x′, S θ). Then T ′ contains the branch θ′ = θN ′, with N ′ = N ∪ {zP x′′}.

Since M, v 6|= x′(R ; P )x′′, we can write M, v |= x′(−(R ; P ))x′′. That is, for every u ∈ U either (v(x′), u) ∈ m(−R) or (u, v(x′′)) ∈ m(−P ). This holds true in particular for the element u¯ ∈ U such that u¯ = v(z) and therefore either M, v |= x′(−R)z or M, v |= z(−P )x′′ holds.

We now show that M, v 6|= x′(−R)z. Since M and v falsify N , they falsify each literal in it and, in particular, the literals used to construct x′(−R)z. We show by induction over the structure of x′(−R)z that, if a model M and an evaluation v falsify all the literals in N employed for the Boolean construction of x′(−R)z, then

M and v falsify x′(−R)z. If x′(−R)z is itself a literal, then it is clearly falsified by

M and v. Next, suppose that x′(−R)z is such that nnf(x′(−R)z) = x′(S ∪ T )z, where x′(S ∪ T )z is a BoolN -formula. Then, by definition of BoolN -formula, x′Sz and x′T z are BoolN -formulae too. Thus they trivially have a Boolean construction from the literals in N and, by inductive hypothesis they are falsified by M and v. Consequently, M and v falsify x′(S ∪ T )z and x′(−R)z. Finally, let x′(−R)z be such that nnf(x′(−R)z) = x′(S ∩ T )z, with x′(S ∩ T )z a BoolN -formula. Then, by definition of BoolN -formula, either x′Sz or x′T z is a BoolN -formula. Thus, either x′Sz or x′T z has a Boolean construction from the literals in N and, by inductive hypothesis, either x′Sz or x T z is falsified by M and v. This is enough to deduce that M and v falsify ′ x′(−R)z as well. system.

Thus, M, v 6|= zP x′′ holds and hence M, v 6|= N ′, M, v 6|= θ′, and M, v 6|= T ′. The preceding lemma yields immediately the soundness of our dual tableau ⊔⊓ Theorem 2. Let xP y be a relational formula of the (∪, ∩ ; )-fragment. If there is a closed proof tree for xP y, then xP y is valid. 4.3

Completeness The notion of open saturated branch θS of a deduction tree T for a formula xP y is defined as in Section 3.2 with the exception of the item relative to ( ; )-formulae that here is formalized as follows: – if x′(R ; P )y′ ∈ N , with N a node of θS, there is an N ′ ∈ θS such that zP y′ ∈ N ′, for every z ∈ V (−R, x′, S θS).

Lemma 5. Let T be a deduction tree for a formula xP y of the (∪, ∩ ; )-fragment of RL( 1 ). If θS is a saturated open branch of T , then there exist a model M = (U, m) and an evaluation v that falsify θS.

Proof: Let us construct a model M = (U, m) and an evaluation v falsifying every node of the branch θS. Let WθS be the collection of all the variables occurring in the formulae of the nodes of θS . Then we put U =Def WθS and v(x) =Def x, for every x ∈ U .

Let Lit θS be the set of all literals occurring in the nodes of θS. The interpretation m is defined by (x′, y′) ∈/ m(R) if and only if x′Ry′ ∈ Lit θS . m is well defined since, by definition of open saturated branch, if x′Ry′ (resp., x′(−R)y′) occurs in a node of θS, then x′(−R)y′ (resp., x′Ry′) does not occur in any other node of θS. Next, we prove that M and v falsify each formula in the nodes of θS. For this purpose, it is convenient to introduce the set S θS of all the formulae contained in the nodes of θS, and show that M and v falsify each formula in S θS. Then, since each node N of θS is a subset of S θS, M and v falsify N as well.

Let ϕ be a formula of S θS. The proof is carried out by induction over the structure of ϕ.

– Base case. ϕ is a literal. Clearly, by definition, M and v falsify all the literals in S θS (in fact they falsify all the literals in the nodes of θS). – Inductive step. For simplicity, we report the proof only for the case ϕ = x′(R ; Q)y′, in which case x′(R ; Q)y′ ∈ N , for some node N of θS. To prove that M, v 6|= x′(R ; Q)y′, we have to show that for every z ∈ U (that is, z ∈ WθS )

M, v |= x′(−R)z or M, v |= z(−Q)y′ ( 1 ) holds (recall that v(x) = x, for every x ∈ WθS ).

By a repeated application of the ( ; )-rule, all the formulae zQy′, with z ∈ V (−R, x′, θS) occur in S θS. In particular, each of them belongs to a node of the branch and, by inductive hypothesis, M and v do not satisfy all of them. Thus ( 1 ) is satisfied for every z ∈ V (−R, x′, S θS). We have to prove that it holds also for every z ∈ WθS \ V (−R, x′, S θS). In fact we show that if z ∈ WθS \ V (−R, x′, S θS), then M, v |= x′(−R)z. The proof is by induction over the structure of x′(−R)z.

• Base case: x′(−R)z is a literal. Then, x′(−R)z ∈/ S θS . Indeed, if x′(−R)z ∈ S θS then z has to be a member of V (−R, x′, S θS) contradicting our hypothesis. Thus M, v |= x′(−R)z. • In∗duLcettivnensft(exp′(:−wRe)dzi)st=inxg′u(iSsh∪tHhe)zf.oTllohweninxg′t(wSo∪cHas)ezs.has been obtained from the union of x′Sz and of x′Hz. At least one of them, say x′Sz and hence M, v |= x′(−R)z. (without loss of generality), is not a BoolS θS -formula, because otherwise z would belong to V (−R, x′, S θS ). Thus x′Sz does not have a Boolean construction from S θS, z ∈ WθS \ V (S, x′, S θS) and therefore, by inductive hypothesis, M, v |= x′Sz. Thus M, v |= x′(R∪S)z, ∗ Let nnf(x′(−R)z) = x′(S ∩ H)z. Then none of x′Sz and x′Hz are BoolS θS -formulae, because otherwise z would belong to V (−R, x′, S θS). Thus, x′Sz and x′Hz do not have a Boolean construction from S θS and z ∈ (WθS \ V (S, x′, S θS)) ∩ (WθS \ V (H, x′, S θS)). Therefore, by inductive hypothesis, M, v |= x′Sz and M, v |= x′Hz, so that M, v 6|= x′(R ; Q)y′, as we wished to prove.

We haveMsh, ovw|=n xth′(aRt ∩MS,)vz,|=anxd′(−heRn)cze, Mfor, evv|=eryx′z(−∈RW)zθ.S \ V (−R, x′, S θS), and that M, v |= z(−Q)y, for every z ∈ V (−R, x′, S θS). Consequently, for every z ∈ WθS either M, v |= x′(−R)z or M, v |= z(−Q)y′ and therefore of RL( 1 ) then there is a closed proof tree for xP y.

Theorem 3 (Completeness). If xP y is a valid formula of the (∪, ∩ ; )-fragment Proof: Suppose by way of contradiction that there is no closed proof tree for xP y. Let TS a proof tree produced by the procedure described above, such that all leaves are closed or not further expandible. Since TS is not closed, there must be a branch θS of TS that is not closed. Thus θS is an open, saturated branch, since it is not further expandible. Thus, by Lemma 5, there is a model M and an evaluation v falsifying each node of θS. This holds in particular for the root {xP y}, thus contradicting the hypothesis. ⊔⊓ ⊔⊓ 4.4

Termination The proof of termination of the proof procedure described in Section 4.1 can be carried out as in Section 3.2. The proof of Lemma 1 can be easily adapted to this context by observing that: (a) in formulae of type x(−(R ; S))y, the term −R is always a Boolean term.

Consequently the formula x(−R)z originated by the (− ; )-decomposition of x(−(R ; S))y can be decomposed only a finite number of times. (b) There is a finite number of formulae with left variable w that are obtained by applications of the ( ; )-decomposition rule: we observe that the variable w has been introduced by the (− ; )-decomposition of a formula z(−(R ; H))y. By the side conditions of the (− ; )-decomposition rule, the literals on the branch θS with right variable w can only have z as the left variable. Thus, the formulae of type ( ; ) that can be decomposed using the variable w must have z as the left variable and therefore, by the inductive hypothesis they have to be finite in number. By the strictness hypotheses it follows that the number of formulae with left variable w originated from ( ; )-decomposition is finite.

Conclusions and future work

We have presented decision procedures based on the method of dual tableaux for two fragments of the relational logic RL( 1 ). These fragments, called the (r ; )and the (∪, ∩ ; )-fragments, are characterized by the fact that they allow only a restricted application of the composition operator “ ; ”. In particular, in every term of type R ; S, the left argument R can be either a relational variable (for the (r ; )-fragment) or a positive Boolean term (for the (∪, ∩ ; )-fragment).

The decision procedures have been drawn from the dual tableau system for RL( 1 ) presented in [12] by strengthening the side conditions of the ( ; )decomposition rule in such a way as to reduce the collection of object variables that can be used at each decomposition step.

In a forthcoming paper we present the detailed proofs of soundness and completeness of the (r ; )-fragment and decision procedures for some other fragments of RL( 1 ), in particular for a fragment that admits terms of type R; S, where R can be any Boolean term with converse operation.

We plan to provide the complexity analysis for the decision procedures presented in the paper. Our aim is also to check the possibility of improving them by introducing, for instance, a more liberal application of the (− ; )-decomposition rule, or by adding further strictness hypotheses to the proof tree construction process.

We also intend to investigate other extensions of the fragments considered here which allow relational terms containing constant relations with properties such as reflexivity, transitivity, symmetry, and so on. This will permit the definition of dual tableau-based decision procedures for the relational renderings of modal logics such as B, T, S4, of intuitionistic logics, information logics, and context logics, such as the ones reported in [12]. We also plan to explore the possibility of importing into the relational context techniques and strategies used to prove and optimize decidability results in the field of computable set theory, such as the model checking technique introduced in [5] or the small model construction approach described in [6].

References

1. F. Baader . Description logics . In: Reasoning Web: Semantic Technologies for Information Systems, 5th International Summer School. Lecture Notes in Computer Science 5689 , 2009 , pp. 1 - 39 .

2. F. Baader , D. Calvanese , D. L. McGuinness , D. Nardi , P. Patel-Schneider . The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, 2003 .

3. D. Bresolin , private communication, 2007 .

4. C. Brink , K. Britz , and R. A. Schmidt . Peirce algebras . Formal Aspects of Computing , 6 ( 3 ): 339 - 358 , 1994 .

5. D. Cantone . A fast saturation strategy for set-theoretic tableaux . In: TABLEAUX '97: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , pp. 122 - 137 , London, UK, 1997 . SpringerVerlag.

6. D. Cantone , M. Nicolosi Asmundo . On the satisfiability problem for a 3-level quantified syllogistic . In: Proceedings of CEDAR'08 , Sydney , Australia, 11 August, 2008 , pp. 1 - 16 .

7. A. Formisano , E. Omodeo , E. Orlowska . A PROLOG tool for relational translation of modal logics: A front-end for relational proof systems . In: B. Beckert (ed) TABLEAUX 2005 Position Papers and Tutorial Descriptions , Universit¨at Koblenz-Landau, Fachberichte Informatik No 12 , 2005 , pp. 1 - 10 .

8. J. Golin ´ska- Pilarek , E. Munoz-Velasco , and A. Mora . A new decision procedure for modal logic K . In: Proceedings of the International Conference on Computational and Mathematical Methods in Science and Engineering, CMMSE 2009 , pp. 537 - 548 .

9. J. Golin ´ska- Pilarek , E. Orlowska . Tableaux and dual tableaux: Transformation of proofs . Studia Logica , 85 ( 3 ): 283 - 302 , 2007 .

10. R. Maddux . Relation algebras . In: C. Brink , W. Kahl and G. Schmidt (eds.) Relational Methods in Computer Science. Advances in Computer Science. Springer: Wien, New York ( 1997 ).

11. E. Orlowska. Relational interpretation of modal logics . In: H. Andreka , D. Monk , and I. Nemeti eds., Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai , vol. 54 , pp. 443 - 471 , North Holland, 1988 .

12. E. Orlowska, J. Golin´ska-Pilarek. Dual Tableaux: Foundations, Methodology, Case Studies. Book submitted.

13. C. S. Peirce . Note B: the logic of relatives . In: C. S. Peirce (ed) Studies in Logic by Members of the Johns Hopkins University , Little, Brown, and Co., Boston, pp. 187 - 203 ( 1883 ).

14. R. A. Schmidt , E. Orlowska, and U. Hustadt . Two proof systems for Peirce algebras . In: R. Berghammer , B. M¨oller , and G. Struth, (eds.). Relational and KleeneAlgebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra , Bad Malente, Germany, May 12-17, 2003 , Revised Selected Papers, Lecture Notes in Computer Sciencce 3051 , Springer, 2004 , pp. 238 - 251 .

15. A. Tarski . On the calculus of relations . Journal of Symbolic Logic , 6 ( 3 ): 73 - 89 , 1941 .

16. A. Tarski , S. Givant . A Formalization of Set Theory without Variables . American Mathematical Society Colloquium Publications , Providence, Rhode Island, 1987 .