A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation

Abstract

We present a first result towards the use of entailment inside relational dual tableau-based decision procedures. To this end, we introduce a fragment of RL(1), called ({1, [ , }\ ; ), which admits a restricted form of composition. We prove the decidability of the ({1, [ , }\ ; )fragment by defining a dual tableau-based decision procedure with a suitable blocking mechanism and where the decomposition rules for compositional formulae are modified so as to deal with the constant 1 while preserving termination. The ({1, [ , }\ ; )-fragment properly includes the logics presented in previous work and, therefore, it allows one to express, among others, the multi-modal logic K with union and intersection of accessibility relations and the description logic ALC with union and intersection of roles.

-

The relational representation of various non-classical propositional logics has been systematically analyzed in the last decades [16]. A uniform relational framework based on the logic of binary relations RL( 1 ), presented in [15] and called relational dual tableau, showed to be an ee↵ctive logical means to represent in a modular way three fundamental components of a formal system: its syntax, semantics, and deduction system. Relational systems have been defined for modal and intuitionistic logics, for relevant and many-valued logics, for reasoning in logics of information and data analysis, for reasoning about time and space, etc.

The formalization of non-classical logics in RL( 1 ) is based on the fact that once the Kripke-style semantics of the logic under consideration is known, formulae can be treated as relations. In particular, since in Kripke-style semantics formulae are interpreted as collections of objects, in their relational representation they are seen as right ideal relations. In the case of binary relations this means that (R ; 1) = R is satisfied, where ‘;’ is the composition operation on binary relations and ‘1’ is the universal relation.

One of the most useful features of the relational methodology is that, given a logic with a relational formalization, we can construct its relational dual tableau in a systematic and modular way.

Though the relational logic RL( 1 ) is undecidable, it contains several decidable fragments. In many cases, however, dual tableau proof systems are not decision procedures for decidable fragments of RL( 1 ). This is mainly due to the way decomposition and specific rules are defined and also to the strategy of proof construction.

Over the years, great eo↵rts have been spent to construct dua l tableau proof systems for various logics known to be decidable; little care has been taken, however, to design dual tableau-based decision procedures for them. On the other hand, it is well known that when a proof system is designed and implemented, it is important to have decision procedures for decidable logics. In [10], for example, an optimized relational dual tableau for RL( 1 ), based on Binary Decision Graphs, has been implemented. However, such an implementation turns out not to be ee↵ctive for decidable fragments.

As far as we know, relational dual tableau-based decision procedures can be found in [16] for fragments of RL( 1 ) corresponding to the class of first-order formulae in prenex normal form with universal quantifiers only; in [12, 13] for the relational logic corresponding to the modal logic K; in [4, 5] for fragments of RL characterized by some restrictions in terms of type (R ; S); in [11] for a class of relational logics admitting a single relational constant with the properties of reflexivity, transitivity, and heredity; and in [3] for a class of relational fragments extending the ones introduced in [11] by allowing a countable infinity of relational constants with the properties of reflexivity, transitivity, and heredity.

Throughout the paper terms of type (R ; S) will be referred to as compositional terms. Similarly, formulae with compositional terms will be referred to as compositional formulae.

In some cases, like in [11] and in [3], fragments with relational constants satisfying some fixed properties are considered. Therefore, dual tableau-based decision procedures are endowed with specific rules to treat relational constants and their properties. The design of specific rules often needs much care in order to guarantee termination of the related proof procedure. This task is delicate especially when the proof system provides several specific rules for die↵rent relational constants, and when the relational constants are related to one another.

An alternative way to treat properties of relational constants and variables, and of relations between them, is to use relational entailment. Relational entailment can be formalized in the logic RL( 1 ) as follows. Given relations R, R1, . . . , Rn, with n 1, one has that R1=1, . . . , Rn=1 imply R=1 in a model if and only if (1 ; (–(R1 \ . . . \ Rn)) ; 1) [ R=1 holds. It means that entailment is expressible as a term of the language of logic RL( 1 ) and, as a consequence, any validity checker for RL( 1 ) can also be applied to entailment verification.

Introduction of entailment inside relational proof systems allows one to eliminate specific rules and, consequently, to keep the set of decomposition rules small. This approach can be convenient in implementations of automated theorem provers provided that decomposition rules and their application strategy are designed in a suitable way. In its relational formalization, however, entailment involves the universal constant 1 on the left hand side and on the right hand side of compositional terms. Thus, the design of a relational dual tableau-based decision procedure where entailment is admitted is a challenging task that requires special care.

In this paper we present a first result towards the use of entailment inside relational dual tableau-based decision procedures. To this purpose, we introduce a fragment of RL( 1 ), called ({1, [ , }\ ; ), admitting a restricted form of composition where the left subterm R of any term of type (R ; S) is allowed to be either the constant 1 or any term constructed from the relational variables by applying only the operators of relational intersection and union. Similarly, terms of type (R ; 1) are admitted only if R is a Boolean term involving relational variables and the operators of intersection and union.

We prove that the ({1, [ , }\ ; )-fragment is decidable by defining a dual tableau-based decision procedure where a suitable blocking mechanism has been introduced and rules for compositional and complemented compositional formulae have been appropriately modified to deal with the constant 1 while preserving termination.

Such fragment properly includes the logics presented in [4] and, therefore, it can express the multi-modal logic K with union and intersection of accessibility relations and the description logic ALC with union and intersection of roles. Furthemore it can also express, via entailment, properties of the form ‘r ✓ –(s1 [ s2)’ and ‘(s1 [ s2) ✓ – r’, where r, s1, and s2 are relational variables.

The rest of the paper is organized as follows. In Sect. 2 we briefly review the syntax and semantics of the relational logic RL( 1 ) together with its dual tableau and in Sect. 3 we introduce some useful notions which will be used throughout the paper. Then in Sect. 4 we present the ({1, [ , }\ ; )-fragment and its dual tableau-based decision procedure. Finally, in Sect. 5, we draw our conclusions and give some hints for future work. 2

The Relational Logic RL( 1 ) and its Dual Tableau In this section we review the logic RL( 1 ) and its dual tableau in full extent (see also [5] and [16]).

Let RV be a countably infinite set of relational variables p, q, r, s, . . . and let 1 be a relational constant. Then, the set RT of relational terms of RL( 1 ) is the smallest set of terms (with respect to inclusion) built from relational variables and the relational constant 1 with the relational operators ‘\ ’, ‘[ ’, ‘;’ (binary) and ‘–’, ‘ `’ (unary).

Let OV be a countably infinite set of object (individual) variables x, y, z, w, . . .. Then, RL( 1 )-formulae have the form xRy, where x, y 2 OV and R 2 RT. RL( 1 )formulae of type x1y and xry, with r 2 RV, are called atomic RL( 1 )-formulae. A literal is either an atomic formula or its complementation (namely a formula of type x(– 1)y or x(– r)y). For a relational operator ‘]’ other than ‘–’, by a (])term we mean a relational term whose lead operator is ‘]’, and by a (– ])-term we denote a complemented (])-term. For example, the term (r1 [ s) \ (– r2 ; s) is a (\ )-term and has ‘\ ’ as its lead operator, whereas –((r1 [ s) \ (– r2 ; s)) is a (– \ )-term. A (])-formula (resp., (– ])-formula) is a formula whose relational term is a (])-term (resp., (– ])-term). A Boolean term is a relational term built from relational variables with the Boolean operators ‘–’, ‘[ ’, and ‘\ ’. A positive Boolean term is a Boolean term in which the operator – does not occur.

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 homomorphically 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)

= {(a, b) 2 U ⇥ U : (a, c) 2 m(R) and (c, b) 2 m(S), for some c 2 U }; – m(R`) = (m(R))` = {(b, a) 2 U ⇥ U : (a, b) 2 m(R)}.

Let M = (U, m) be an RL( 1 )-model. A valuation in M is any function v : OV ! U . An RL( 1 )-formula xRy is satisfied by an RL( 1 )-model M = (U, m) and by a valuation v in M (in which case we write M, v |= xRy) provided that (v(x), v(y)) 2 m(R). An RL( 1 )-formula xRy is (a) true in a model M = (U, m), if M, v |= xRy, for every valuation v in M; (b) valid, if it is true in all RL( 1 )models; (c) falsified by a model M = (U, m) and by a valuation v in M, if M, v 6|= xRy; (d) falsifiable, if there exist a model M and a valuation v in M such that M, v 6|= xRy. An RL( 1 )-set is a finite set {' 1, . . . , ' n} of RL( 1 )formulae such that, for every RL( 1 )-model M and for every valuation v in M, we have M, v |= ' i, for some i 2 { 1, . . . , n}. Clearly, the first-order disjunction of the formulae in an RL( 1 )-set is valid in first-order logic.

Proof development in dual tableaux proceeds by systematically decomposing the (disjunction of the) formula(e) to be proved till a validity condition is detected, expressed in terms of axiomatic sets (see below). The method originated in [17] (see also [18]). Such an analytic approach is similar to Beth’s tableau method [1], with the die↵rence that the two systems work in a dual ma nner. Duality between tableaux and dual tableaux has been analyzed in depth in [14].

RL( 1 )-dual tableaux consist of decomposition rules, which allow one to analyze the structure of the formula to be proved valid, and of axiomatic sets, which specify closure conditions. The decomposition rules for RL( 1 ) are listed in Table 1. In these rules, ‘,’ and ‘|’ are interpreted respectively as disjunction and conjunction. A rule is RL( 1 )-correct provided that its premise is an RL( 1 )-set if and only if each of its consequents is an RL( 1 )-set. The rules presented in Table 1 have been proved RL( 1 )-correct in [16].

An RL( 1 )-axiomatic set is any set of RL( 1 )-formulae containing a subset of one of the following two forms: (Ax 1){xRy, x(– R)y}, (Ax 2) {x1y}.

Clearly, an RL( 1 )-axiomatic set is also an RL( 1 )-set.

An RL( 1 )-proof tree for an RL( 1 )-formula xP y is an ordered tree whose nodes are labelled by disjunctive sets of formulae such that the following properties are satisfied: – the root is labelled with {xP y};

A branch ✓ of a proof tree is any of its maximal paths; we denote with S ✓ the set of all the formulae contained in the nodes of ✓ , and with W✓ the collection of the object variables occurring in the formulae contained in the nodes of ✓ . A node of an RL( 1 )-proof tree is closed if its associated set of formulae is 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 RL( 1 )-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 a valuation v in M if every formula xRy in its set of formulae is falsified by M and v. A node is falsifiable if there exist a model M and a valuation v in M which falsify it.

Correctness and completeness of the RL( 1 )-dual tableau are proved in [16]. However, the logic RL( 1 ) is undecidable. This follows from the undecidability of the equational theory of representable relation algebras discussed in [19]. 3

Useful Notions and Properties We introduce some useful notions and properties which are needed for the presentation of the results of the paper.

Let P be any relational term in RL( 1 ). The following identities hold: (1 [ P ) ⌘ (P [ 1) ⌘ 1 (1 \ P ) ⌘ (P \ 1) ⌘ P (–(– 1)) ⌘ 1 ((– 1) [ P ) ⌘ (P [ (– 1)) ⌘ P ((– 1) \ P ) ⌘ (P \ (– 1)) ⌘ (– 1) Let H be a relational term in RL( 1 ) and let H0 be obtained from H by systematically simplifying H by means of the above identities. If the simplification is carried out in an inside-out way, the computational complexity of the transformation of H into H0 is linear in the length of H. Moreover, the following lemma holds (proof of Lemma 1 can be found in [6]).

Lemma 1. Let H be a relational term and let H0 be constructed as outlined above. Then every Boolean subterm P of H0 either is equal to 1, or is equal to – 1, or it does not contain 1.

It is easy to check that m(H) = m(H0) holds for every RL( 1 )-model M = (U, m) and for every H 2 RL( 1 ). Therefore we can restrict ourselves to relational terms simplified as described above.

Parsing trees. It is possible to associate a parsing tree SP to each relational term P of RL( 1 ), as with formulae of standard first-order logic (see [9] and [8] for details on the construction of parsing trees in first-order logic). Let SP be the parsing tree for P , and let ⌫ be a node of SP . We say that a relational term Q occurs within P at position ⌫ if the subtree of SP rooted at ⌫ is identical to SQ. In this case we refer to ⌫ as an occurrence of Q in P and to the path from the root of SP to ⌫ as its occurrence path.

An occurrence of a relational term Q within a relational term P is positive if its occurrence path deprived of its last node contains an even number of nodes labelled with {–}. Otherwise, the occurrence is said to be negative. Normal forms and term components. Next we introduce the notion of complement normal form for Boolean relational terms, the notions of BoolN formula, of Bool-construction from N , where N is a set of formulae, and of set of components of a relational term.

The complement normal form of a term R is a term nf–(R) obtained by successive applications of the De Morgan laws and of the law of double negation to R.

A term is said to be in complement normal form whenever each occurrence of the complement operator in it acts only on relational variables or constants.

Clearly, for every Boolean relational term R, the formulae xR y and x nf–(R) y are logically equivalent, that is M, v |= xRy if and only if M, v |= x nf–(R)y, for every model M = (U, m) and every valuation v in M.

Let N be a set of formulae, and let R, S be two Boolean relational terms. We define the notion of BoolN -formulae as follows: – every literal xRy in N is a BoolN -formula; – every formula of the form x(R \ S)y is a BoolN -formula, provided that either xRy is a BoolN -formula and S is in complement normal form, or xSy is a BoolN -formula and R is in complement normal form; – every formula of the form x(R [ S)y is a BoolN -formula if both xRy and xSy are BoolN -formulae. Clearly, if xSy is a BoolN -formula, then xSy is syntactically equal to x nf–(S) y and we write xSy = x nf–(S) y. We say that a formula xRy has a Boolconstruction from N if x nf–(R) y is a BoolN -formula.

For example, given the set of formulae N = {x(– r)z, xsz, x(– p)y, z(p [ s)y}, we have that the formula x(((– r)[ s)\ q)z is a BoolN -formula because x((– r)[ s)z is a BoolN -formula and xqz is in complement normal form. On the other hand the formula x(s \ (–(q [ p)))z is not a BoolN -formula because although xsz is a BoolN -formula, x(–(q \ p))z is not in complement normal form. Both formulae, however, have a Bool-construction from N because x(((– r) [ s) \ q)z is a BoolN formula and x nf–(s \ (–(q [ p)))z = x(s \ ((– q) \ (– p)))z is a BoolN -formula. In this latter case, specifically, xsz is a BoolN -formula and x((– q) \ (– p))z is in complement normal form, although it is not a BoolN -formula.

Given a term R in RT, an object variable x, and a set N of formulae, we define V (R, x, N ) as the set of object variables z such that xRz has a Bool-construction from N .

Let P be a term in RT. We define recursively the set cp(P ) of the components of the term P as follows: – if P is the relational constant 1, or a relational variable, or their complements, then cp(P ) = {P }; – if P = – – B, then cp(P ) = {P } [ cp(B); – if P = B`, then cp(P ) = {P } [ cp(B); – if P = B ] C (resp., P = –(B ] C)), then cp(P ) = {P } [ cp(B) [ cp(C) (resp., cp(P ) = {P } [ cp(– B) [ cp(– C)), for every binary relational operator ]. Clearly cp(P ) is finite, for any relational term P .

; ) and its Decision Procedure 4 4.1

The Fragment ({1, [ , }\

The Fragment ({1, [ , \}

; ) Formulae of the fragment ({1, [ , }\ ; ) of RL( 1 ) are characterized by the fact that the left subterm R of any term of type (R ; S) in them is only allowed to be either the constant 1 or a term constructed from the relational variables of RV by applying only the ‘[ ’ and ‘\ ’ operators, whereas the right subterm S of (R ; S) can involve all the relational operators of RL( 1 ) but the converse operator ‘ `’.

Formally, the set RT({1,[ ,\} ; ) of the terms allowed in ({1, [ , }\ ; )-formulae is the smallest set of terms containing the constant 1 and the variables in RV, and such that if P, Q, B, H 2 RT({1,[ ,\} ; ) and S 2 { H, 1}, with – B a Boolean term containing neither 1 nor the complement operator, and – H containing the constant 1 only inside terms of type (B ; 1), then (– P ), (P [ Q), (P \ Q), (B ; S), (1 ; S) 2 RT({1,[ ,\} ; ).

Examples of formulae of the ({1, [ , }\ ; )-fragment are: x(–((r1 [ s) ; (p ; 1)))y, x(1 ; ((r1 [ s) ; –(((q [ p) \ r1) ; 1)))y, and x(1 ; (((r1 [ s) \ r2) ; 1))y. The latter formula can be rewritten as x(1 ; (–(–(r1 [ s) [ – r2) ; 1))y, where (–(r1 [ s) [ – r2) is a relational term formalizing the property ‘(r1 [ s) ✓ – r2’. The decomposition rules for Boolean formulae of our dual tableau-based calculus are just the ones in Table 1. Concerning the decomposition rule for (;)-formulae, it is convenient to distinguish between (;)-formulae of type x(B ; S)y and of type x(1 ; S)y. The rule for (;)-formulae of type x(B ; S)y is the (;)a -rule of Table 2. There, z is an object variable belonging to V (– B, x, N ), where N stands for the current node. Notice that if S = 1, the node resulting from the decomposition step is axiomatic. In case of (;)-formulae of type x(1 ; S)y, we apply the rule (;)b in Table 2. The variable z used in rule (;)b is any variable on the current node, provided that the current branch does not already contain the formula zSy. Otherwise, x(1 ; S)y cannot be decomposed with z. If S = 1, the same remark made for rule (;)a , for the node resulting from the decomposition step, holds here as well.

Concerning (– ;)-formulae, we consider first the case of formulae of type x –(B ; S)y. If S 6= 1, such formulae are decomposed by means of the (– ;)rule in Table 1. Otherwise, when S = 1, we use the rule (– ;)a of Table 2. In the case of formulae of type x –(1 ; S)y, with S 6= 1, we use instead the rule (– ;)b of Table 2, with z an object variable new to the current node. The rule can be applied provided that the current branch does not contain any formula of the form z0(– S)y, for any ‘new’ variable z0 (otherwise, the formula x –(1 ; S)y cannot be decomposed). The formula x(–(1 ; 1))y is not decomposed.

Some remarks on the rules (;)a , (;)b , (– ;)a , and (– ;)b in Table 2 are in order. The idea behind the definition of the side condition of the rule (;)a takes inspiration from the side condition of expansion rules for universally quantified formulae present in various well known tableau-based proof systems (see for instance [2]). The introduction of the set V (– B, x, N ) is motivated by the fact that our relational fragment admits compositional terms (B ; S), where B may be a compound term. Observe that for every RL( 1 )-model M = (U, m), m( 1 ) = U ⇥ U so that, M, v |= x1z and M, v 6|= x(– 1)z hold, for every valuation v and object variables x and z. Thus, we shall assume without loss of generality that each node of any dual tableau for formulae of the ({1, [ , }\ ; )-fragment contains implicitly all literals of type x(– 1)z. This accounts for the fact that the decomposition rules (– ;)a and (– ;)b do not introduce z(– 1)y and x0(– 1)z, respectively, on the new node, and rule (;)b restricts z to be any variable on the current node, rather than any possible variable. At any rate, we shall prove that such a restriction preserves the completeness of the procedure.

It is convenient to introduce the notion of deduction tree for RL( 1 )-formulae to give a step-by-step description of the proof tree construction process.

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 will be 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 ({1, [ , }\ ; )-formula. 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.3 The tree obtained from T by applying to N either one of the decomposition rules in Table 1 (for Boolean formulae and for (– ;)-formulae of type x0 –(B ; S)y, with S 6= 1), or one of the decomposition rules in Table 2 (for (;)-formulae and for (– ;)-formulae of type x0 –(B ; 1)y and of type x –(1 ; S)y) is a deduction tree for xP y. More precisely, rules applications are described as follows: • if a formula x0Qy occurs in N and a rule with a single conclusion set of formulae (resp., a branching rule with the conclusion sets 1 and 2) is applicable to x0Qy, then we append the node N 0 = (N \ {x0Qy}) [ as the successor of N in ✓ (resp., the node N10 = (N \ {x0Qy}) [ 1 as the left successor of N and the node N20 = (N \ {x0Qy}) [ 2 as the right successor of N in ✓ ).

Given a branch ✓ of a deduction tree, each object variable in W✓ \ {x, y} is generated by an application of a (– ;)-decomposition rule. We say that a variable w is an ancestor of degree n of a variable z 2 W✓ \ {x, y} if there is a sequence z1, . . . , zn of variables in W✓ \ {x, y}, with zn = z and n 1, such that z1 is generated by a (– ;)-formula w(–(B0 ; S0))y, z2 is generated by a (– ;)-formula z1(–(B1;S1))y,..., zn is generated by a (– ;)-formula zn 1(–(Bn 1 ;Sn 1))y, where w(–(B0 ; S0))y, z1(–(B1 ; S1))y,..., zn 1(–(Bn 1 ; Sn 1))y are formulae of ✓ . In such a case, we say that z1 is a descendant of degree 1 of w and that zn = z is a descendant of degree n of w.

It is useful to define a total order <✓ among variables in W✓ such that: – x <✓ w, for every w 2 W✓ \ {x}, – x1 <✓ x2, for every x1, x2 2 W✓ \ {x, y}, with x1 introduced in ✓ before x2, – y <✓ z, for every z descendant of y, – w <✓ y, for every w that is not a descendant of y. 3 From now on, we identify nodes with the (disjunctive) sets labelling them. Remark 1. Notice that the relationship ancestor/descendant is based on the literals of type x0(– r)z that are generated by applying either the (– ;)-rule of Table 1 or the (– ;)a -rule of Table 2, and, possibly, the Boolean decomposition rules. Remark 2. By the construction of RT({1,[ ,\} ; ), a deduction tree for a formula xP y may contain formulae of type x(1;S1)y and of type x(–(1;S2))y only if their left variable is x. This is motivated by the fact that each of these formulae can be obtained only by the Boolean decomposition of xP y. Any variable z resulting from the decomposition of a (– ;)-formula of type x(–(1 ; S))y is not a descendant of x. However, according to the definition of the order <✓ , x <✓ z holds. The following notions will be used in the next section to turn our tableau calculus for ({1, [ , }\ ; ) into a terminating proof tree construction procedure.

Let ✓ be a branch of a deduction tree, and let z(–(B ; S))y and z0(–(B ; S))y be two (– ;)-formulae occurring in ✓ . We say that z0(–(B ; S))y blocks z(–(B ; S))y (and that z(–(B ; S))y is blocked by z0(–(B ; S))y), if the following conditions are satisfied: – z(–(B ; S))y and z0(–(B ; S))y are identical with the exception of the left object variable, – z0(–(B ; S))y has been already decomposed in ✓ using the variable w, – for every (;)-formula z(B1 ;Q)y occurring in ✓ such that z(– B1)w has a Boolconstruction from the set of literals resulting from the Boolean decomposition of z(– B)w, the (;)-formula z0(B1 ; Q)y occurs in ✓ as well. 4.3

A Proof Tree Construction Procedure for ({1, [ , \} ; ) Starting with an initial deduction tree T0 for a given formula xP y, the following procedure constructs a proof tree for xP y. 1. For every non-axiomatic branch ✓ of the current deduction tree, 2. while ✓ is non-axiomatic and is further expandable, let z be the smallest variable w.r.t. <✓ such that formulae on ✓ with left variable z have not been decomposed in ✓ . Apply to the formulae on ✓ having left variable z the decomposition rules in the following order: Boolean rules, (– ;)-rules, rule (;)a , and then apply rule (;)b to decompose the (;)-formulae of type x(1 ; S)y in ✓ with the variable z in a systematic way under the following restrictions: a. all the rules can be applied at most once with the same premise; b. every formula of type (– ;), z(–(B ; S))y is not decomposed provided that it is blocked by a (– ;)-formula z0(–(B ; S))y occurring in ✓ .

If z0(–(B ; S))y was decomposed in ✓ with the variable w, then for every literal z0(– r)w 2 S ✓ (obtained from the application of the Boolean rules to z0(– B)w) we store the literal z(– r)w in Lit (– ;), a set (empty at the beginning of the execution of the procedure) collecting literals not explicitly occurring in ✓ that are needed to construct M✓ (see step 4). 3. If the branch ✓ is axiomatic and all the other branches on the current deduction tree are axiomatic, then the current deduction tree is a proof tree for xP y and we terminate. Otherwise, if the branch ✓ is axiomatic and there are still non-axiomatic branches on the current deduction tree, return to step 1. 4. Otherwise, if ✓ is non-axiomatic, namely it is a non-axiomatic not further expandable branch, we construct from ✓ the model M✓ = (U✓ , m✓ ) defined as follows. We put U✓ = W✓ . Next, let Lit ✓ be the set of all literals occurring in ✓ , and let Lit (– ;) be defined as in step 2. We define the interpretation M✓ by putting (x0, y0) 2 / m✓ (R) if and only if x0Ry0 2 (Lit ✓ [ Lit (– ;)). Let v✓ : OV ! U✓ be a valuation such that v✓ (x) =Def x, for every x 2 U✓ . We terminate returning ✓ , M✓ , and v✓ .

The next lemma states two useful properties of the formulae occurring on the deduction trees constructed by the proof procedure above. Its proof can be carried out by induction on proof construction and by case distinction on the structure of x0Rx00.

Lemma 2. Let T be a deduction tree for xP y constructed by an execution of the procedure described above. If x0Rx00 is a formula of a branch ✓ of T , then (i) R 2 cp(P ), and (ii) if R contains the composition operator, then x00 = y. Termination of the procedure. Let T be a proof tree for a formula xP y of the ({1, [ , }\ ; )-fragment constructed according to our proof-tree construction procedure. To prove that our procedure always terminates, we show that any branch of T can be constructed in a finite number of steps. We mainly focus on non-axiomatic not further expandable branches, since in the case of axiomatic branches the proof is straightforward. To begin with, we characterize a nonaxiomatic not further expandable branch ✓ of T as a non-axiomatic branch such that all the rules applicable to the formulas occurring on its nodes have been applied following the steps of the given decision procedure.

Next we state some preliminary lemmas and remarks useful to show that ✓ contains a finite number of formulae. Lemma 3 is a technical lemma used to prove Lemmas 4 and 5 which, in their turn, are used in Lemma 6 to show that (;)-formulae, the only formulae that can be decomposed more than once, are decomposed a finite number of times. Lemma 4 is proved by showing that the set V (– B, w, N ) is finite, where N is the leaf node of ✓ . The proof of Lemma 5 uses the fact that cp(P ) is finite (Lemma 2), the fact that for every x0 2 W✓ , S ✓ contains a finite number of formulae of type x0Rx00 (Lemma 3), and the blocking mechanism introduced in Sect. 4.2. The interested reader may find the proofs of Lemmas 3, 4, and 5 in [6].

Lemma 3. Let ✓ be a non-axiomatic not further expandable branch of a proof tree T for a formula xP y. Then, for every x0 2 W✓ , S ✓ contains a finite number of formulae of type x0Rx00.

Remark 3. Variables generated by (– ;)-formulae with left variable y are finitely many because (– ;)-formulae of type y(–(B ; S))y are finitely many too. Moreover these variables are distinct from all the variables generated by the other (– ;)formulae because each application of the (– ;)-rule introduces a new variable. Remark 4. If a variable w is generated by a (– ;)-formula x0(–(B ; S))y with x0 6= y, then no literal of the form y(– r)w is in ✓ . In fact, by Lemma 3 we know that literals of type y(– r)z, with z 6= y, are introduced in ✓ only after the decomposition of a (– ;)-formula with left variable y. But then z cannot be the same variable introduced by a (– ;)-formula x0(–(B ; S))y with x0 6= y. Remark 5. Every (;)-formula w(B ;S)y is decomposed only with the variables introduced by the decomposition of (– ;)-formulae with left variable w and possibly with the variable y.

Lemma 4. Every formula w(B ;S)y in ✓ is decomposed a finite number of times. Lemma 5. W✓ is finite.

Next, we define recursively the weight of a term by putting: – weight (r) = weight (– r) = weight ( 1 ) = weight (– 1) = 0; – weight (A ] P ) = weight (A) + weight (P ) + 1, for ] 2 {[ , \ , ;}; – weight (–(A ] P )) = weight (– A) + weight (– P ) + 1, for ] 2 {[ – weight (– – P ) = weight (P ) + 1. , \ , ;}; Then the weight of a formula xP y is defined as the weight of its term P and the weight of a node N is defined as the sum of the weights of the formulae in N . In particular, the weight of every (;)-formula and the weight of every (– ;)-formula that cannot be decomposed in N , according to the decomposition rules and, in particular, to the conditions on rules application stated in step 2, is set to 0. It can be checked that the weight of a node N is 0 if and only if it contains only literals and formulae of types (;) and (– ;) that cannot be further decomposed, according to the definition of the decomposition rules and of the requirements on rules application in step 2 of our proof-tree construction procedure. Thus, a branch with leaf node of weight 0 is not further expandable.

Lemma 6. After a finite number of decomposition steps, a branch ✓ of a deduction tree for xP y is prolonged to a branch which can be either axiomatic or non-axiomatic and whose leaf node has weight equal to 0.

Proof. Let ✓ = ✓ 1, ✓ 2, . . . be such that ✓ i+1 is obtained from ✓ i by an application of a decomposition rule to the leaf node Ni of ✓ i, for i = 1, . . .. If ✓ i happens to be an axiomatic branch, then the thesis immediately follows. Otherwise, we reason as shown next. For every (;)-formula ' of Ni, of both types x0(B ; S)y and x(1 ; S)y, let dec(,' N i) be the number of times ' has been decomposed on the branch to which Ni belongs. If ' = x(1 ; S)y, then dec(,' N i)  | W✓ |. By Lemma 5, |W✓ | is finite and once dec(x(1 ; S)y, Ni) reaches it, weight (x(1 ; S)y) is set to 0. If ' = x0(B ; S)y, then dec(,' N i) is bounded as stated in Lemma 4. It turns out that, at each decomposition step, we have either 1. weight (Ni) > weight (Ni+1), or 2. ⌃ ' 2 Nidec(,' N i) < ⌃ ' 2 Ni+1dec(,' N i+1).

The first condition holds when the decomposition rule applied to ✓ i to produce ✓ i+1 is die↵rent from the ( ;)-rule. In fact the decomposed formula is not introduced in the new node and the components have smaller weights. Moreover, each (– ;)-formula that is blocked gets weight 0. The second condition, on the other hand, holds when the (;)-rule is used. In this case, since the decomposed (;)-formula ' is introduced in the new node, the weight of the new node does not decrease (it could increase), but dec(,' N i) increases and since it is bounded, after a finite number of steps ' is not decomposed anymore getting weight 0.

Since each node contains a finite number of formulae, after a finite number of steps we obtain a branch ✓ n whose leaf node has weight 0. This means that ✓ n is not further expandable. Moreover, if ✓ n is not closed, then it is a non-axiomatic not further expandable branch. In fact, all the Boolean formulae in ✓ n have been decomposed, and, in view of the conditions of step 2 all the (– ;)-formulae either have been decomposed into formulae of smaller weight or have not been decomposed and their weight has been set to 0. Finally, all the (;)-formulae in ✓ n have been decomposed, each finitely many times according to condition (a) of step 2. tu Considering that our proof-tree construction procedure constructs any axiomatic branch and any non-axiomatic not further expandable branch of a proof tree for xP y in a finite number of decomposition steps and that each decomposition rule is finitely branching, we can state the following theorem. fragment always terminates.

Theorem 1 (Termination). The dual tableau procedure for the ({1, [ , }\ ; )(thus, in particular, xP y itself).

Soundness and completeness. Correctness of our proof-tree construction procedure is proved by showing that when the input formula xP y is valid, the procedure yields a closed (axiomatic) dual tableau for xP y, whereas if xP y is not valid, the procedure yields a non-axiomatic not further expandable branch ✓ of a dual tableau for xP y and a model M✓ that falsifies every formula on ✓

Lemma 7, stated below, is used in the proof of Theorem 2 to establish the first half of the correctness proof, and also later, in the proof of Theorem 3.

Lemma 7. Let T be a deduction tree for a formula xP y of the ({1, [ , }\ fragment, constructed as described in our proof-tree construction procedure. If the ; )procedure terminates at step 4 yielding a non-axiomatic not further expandable branch ✓ , a model M✓ = (U✓ , m✓ ), and a valuation v✓ , then M✓ and v✓ falsify Theorem 2. If xP y is a valid formula of the ({1, [ , }\ ; )-fragment of RL( 1 ), then our proof-tree construction procedure yields a closed proof tree for xP y.

Lemma 8, presented next, states that each decomposition step performed by our proof-tree construction procedure preserves falsifiability. This result is needed later in the proof of Theorem 3, to establish the second half of the correctness proof. Proofs of Lemmas 7 and 8 and of Theorems 2 and 3 can be found in [6].

Lemma 8. Let ✓ be a branch of a deduction tree for a formula xP y of the ({1, [ , }\ ; )-fragment that is being constructed by our proof-tree construction procedure, and let ✓ 0 be obtained from ✓ by a decomposition step performed by the decision procedure. If ✓ is a falsifiable branch, then ✓ 0 is falsifiable too. Theorem 3. Let xP y be a non valid relational formula of the ({1, [ , }\ ; )fragment. Then our proof-tree construction procedure yields a non-axiomatic not further expandable branch ✓ of a dual tableau for xP y and a model M✓ that falsifies every formula on ✓ and, therefore, xP y itself.

Summing up, Theorems 2 and 3 yield the following result.

Theorem 4. The ({1, [ , }\ ; )-fragment has a decidable validity problem. 5

Conclusions and Future Work Relational entailment allows one to deal with properties of relational constants and of relational variables in dual tableau proofs without adding any specific rule to the basic set of decomposition rules. Using entailment in dual tableau-based decision procedures, however, can be tricky because the constant 1 occurs both on the left-hand side and on the right-hand side of composition.

We have presented a dual tableau-based decision procedure for a fragment of the logic RL( 1 ) which can express simple forms of inclusion between relations. Specifically, we admit inside entailment only positive occurrences of Boolean terms and thus we can express inclusion properties of the form ‘(r1 [ s) ✓ – r2’.

We plan to extend the expressibility of our relational fragment in order to make entailment widely applicable in dual tableau-based decision procedures. As a first step, we intend to include negative occurrences of Boolean terms inside entailment. In this way we will be able to formulate terms of type 1 ; (–(–(r1 [ s) [ r2) ; 1) expressing the (positive) inclusion property ‘(r1 [ s) ✓ r2’.

Our further aim is to add, inside entailment, some restricted forms of composition so as to be able to express terms of type 1 ; (–(–(s ; s) [ s) ; 1) and of type 1;(–(–(r;r;r)[ r); 1), stating, respectively, that the relational variables s and r are transitive (i.e., ‘(s ; s) ✓ s’) and three-transitive (i.e., ‘(r ; r ; r) ✓ r’), respectively. Expressing these properties is important if one wants to use our dual tableau decision procedure with various non-classical logics such as, for instance, modal logics to reason with incomplete information [7].

We also intend to introduce the converse relation ‘`’ and the identity relation ‘10’ inside entailment for the purpose of dealing with properties such as symmetry and reflexivity. Acknowledgments. Thanks are due to three anonymous referees for their helpful suggestions. This work was supported by Indam-GNCS, Progetto di ricerca “Automi Reattivi e loro Simulazione nell’Ambito del Non-Standard Secure Text Processing”.

References

1. W. E. Beth . Semantic entailment and formal derivability . Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde , N.R . Vol 18 , no 13, 1955 , pp 30942 . Reprinted in Jaakko Hintikka (ed.) The Philosophy of Mathematics , Oxford University Press, 1969 .

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. Cantone , J. Golin´ska- Pilarek , M. Nicolosi-Asmundo . A Relational Dual Tableau Decision Procedure for Multimodal and Description Logics . To appear in: Proceedings of the 9th International Conference on Hybrid Artificial Intelligence Systems , Salamanca, Spain, 11th - 13th June 2014 .

4. D. Cantone , M. Nicolosi Asmundo , E. Orlowska. Dual tableau-based decision procedures for some relational logics . In: Proceedings of the 25th Italian Conference on Computational Logic, Rende, Italy, July 7-9 , 2010 , pp. 1 - 16 . CEUR Workshop Proceedings vol. 598 .

5. D. Cantone , M. Nicolosi Asmundo , E. Orlowska. Dual tableau-based decision procedures for relational logics with restricted composition operator . Journal of Applied Non-classical Logics 21, No 2 , 2011 , 177 - 200 .

6. D. Cantone , M. Nicolosi-Asmundo , E. Orlowska . A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation (extended version) . Available at http://www.dmi.unict.it/⇠ nicolosi/CNOCILC14ext.pdf, 2014 .

7. S. Demri , E. Orlowska , D. Vakarelov . Indiscernibility and complementarity relations in information systems . In: J. Gerbrandy , M. Marx , M. de Rijke and Y. Venema (eds) JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday , Amsterdam University Press, 1999 .

8. N. Dershowitz , J.-P. Jouannaud . Rewrite Systems. Handbook of Theoretical Computer Science , Volume B: Formal Models and Semantics (B). Elsevier . pp. 243 - 320 , 1990 .

9. M.C. Fitting . First-Order Logic and Automated Theorem Proving . Second edition . Graduate Texts in Computer Science. Springer-Verlag. New York, 1996 .

10. A. Formisano and M. Nicolosi Asmundo . An ecient relatio nal deductive system for propositional non-classical logics . Journal of Applied Non-Classical Logics , vol. 16 ( 3-4 ), pp. 367 - 408 ( 2006 ).

11. J. Golin ´ska- Pilarek , T. Huuskonen , E. Munoz-Velasco , Relational dual tableau decision procedures and their applications to modal and intuitionistic logics . Annals of Pure and Applied Logics vol. 165 ( 2 ), pp. 409 - 427 ( 2014 ).

12. J. Golin ´ska- Pilarek , E. Munoz-Velasco , and A. Mora . Implementing a relational theorem prover for modal logic K. International Journal of Computer Mathematics , 88 ( 9 ): 1869 - 1884 , 2011 .

13. J. Golin ´ska- Pilarek , E. Munoz-Velasco , and A. Mora . A new deduction system for deciding validity in modal logic K . Logic Journal of IGPL 19 ( 2 ): 425 - 434 , 2011 .

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

15. 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 .

16. E. Orlowska, J. Golin´ska-Pilarek. Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic vol. 36 , Springer, 2011 .

17. H. Rasiowa , R. Sikorski . On Gentzen theorem . Fundamenta mathematicae 48 , 57 - 69 , 1960 .

18. H. Rasiowa , R. Sikorski . Mathematics of Metamathematics, Polish Scientific Publishers PWN, Warsaw 1963 .

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