Prefixed Tableaux Systems for Modal Logics with Enriched Languages

1 Introduction

The definition of logical formalisms that model cognitive and reasoning processes has been always confronted to two issues: how to decrease the expressive power of ex­ isting untractable logics in order to obtain tractable frag­ ments and how to increase the expressive power of de­ cidable logics while preserving decidability- this includes for instance the extension of known decidable fragments of the classical logic. These fragments include various modal logics (see e.g. [Hughes and Cresswell, HJ84]) if one translates them in the standard way to classical logic. The modal logics have been recognized in the Ar­ tificial Intelligence community as serious candidates to capture different aspects of reasoning about knowledge (see e.g. [Fagin et al., 1995]). However the standard modal logics have a restricted expressive power (for in­ stance the class of irreftexive frames is not definable by a modal formula of the logic K).

That is why in the literature various modal logics with enriched languages have been defined . Most of the work clone for these logics has been dedicated to study their expressive l?ower (see e.g. [Goranko and Passy, 1992; Rijke, 1993J). In the paper our aim is to analyze var­ ious features related to the mechanization of numerous modal logics with enriched languages. To do so, we de­ fine prefixed tableaux which are known to be dose to the semantics of the logics and they allow a user-friendly presentation of the proofs. Moreover , the use of prefixes

*Work supported by C.N.RS., France.

Stephane Demri

Laboratoire LEIBNIZ, 46 A venue Felix Viallet, 38031 Grenoble, France.

(see e.g. [Fitting, 1983; Wallen, 1990; Massacci, 1994; Governatori, 1995]) is known to take advantage of the computational features of the logics. Namely, each pre­ fix occurring at some stage of the proof contains some information about part of the current proof. However we ignore whether a matrix characterization of the log­ ics treated herein exist in order to avoid some redundan­ cies in the tableaux proof search -notational r·edund(mcy, in-elev(mre and non-per·rnutability [Wallen, 1990].

The logics treated in the paper contain various oper­ ators that. differ from the standard necessity operator 0 (also noted [R]):

• the difference operator [#] that allows to access to the worlds different: from the current world (see e.g. applications of its use in [Segerberg, 1981 ; Sain, 1988; Koymans, 1992; Rijke, 1993])
• the complement operator [-R] that allows to access to the worlds not. accessible from the current world (see e.g. [Humberst.one, 1983; Goranko, 1990a; Levesque, 1990; Lakemeyer, 1993])
• and by a side-effect the universal operator [U] that. allows to access to any world of the model (see e.g. [Goranko and Passy, 1992]) . [U]A can be defined in various ways: for instance [U]A =def A 1\ [#]A or [U]A =rteJ [R]A 1\ [-R]A.

Adding these operators to standard modal logics can significantly increase their expressive power. For in­ stance every finite cardinality is definable in a modal logic whose language contains [#] [Koymans, 1992]. Most of the logics dealt with in the paper have a decid­ able sa.tisfiabilit.y problem and we shall provide decision procedures based on our systems. However because of the expressive power of the logics our calculi have two original feat.mes: a current information C is associated to each branch of a tableau and a restricted cut rule is included in various calculi that. can be viewed as a modal variant of the cut rule in the d'Agostino's calculi [d'Agostino, 199:3] .

The rest of the paper is structured as follows. Sec­ tiou 2 presents the logics considered in the paper. The sections :~, 4, ;, and 6 present the calculi for the various logics as well as the decision procedures. Because of lack of space we have omitted part of the proofs a..'> well as the possible extensions where the accessibility relations satisfy standard conditions (reflexivity, symmetry, tran­ sitivity, ... ) . Section 7 compares our calculi with existing ones for other modal logics and concludes the paper by presenting possible extensions.

2 Enriched multi-modal logics

2.1 Syntax and semantics

A modal language L is determined by three sets that are supposed to be pairwise disjoint: a set Foro = {p, q, .. . } of propositional variables, a set {--.,t\} of propositional operators (the connectives V, =>, <=> are defined as for the propositional calculus) and a (possibly finite) countable set OP = {[i] : i E I} of modal operators. The set of formulae For of the language L is defined by the following grammar: A ::= pI -.A I At\B I $A where p E For0 , A, B E For and $ E OP. In the sequel we assume that OP is finite and as usual (i)A =def --.[i]--.A. A frame is a structure (W, (R;)iei) where W is a non-empty set of worlds (sometimes also called knowledge st(Jtes) and (Ri)iei is a family of binary relations on W. A model M is a structure (W, (R;)iei, V) where (W, (R;)iei) is a frame and V is mapping Foro -t P(W), the power set of W. For each set W, we write idw (resp. difw) to denote the binary relation { (w, w) : w E W} (resp. W x W \ idw). Let M = (W, (R;);ei, V) be a model. As usual, we say that a formula A is .5(Jtisfied by the world w E W (den cited by M, w F= A) when the following conditions are satisfied:

• M, w F= p iff wE V(p) for all p E Foro,
• M,w f= -.A iff not M,w f= A,
• M, w f= A t\ B iff M, w f= A and M, w f= B,
• M, w f= [i]A iff for all w' E W such that (w, w') E R;, we have M, w' f= A.

In the sequel by a logic C we understand a pair (For, S) such that For is a set of formulae from a given language and Sis a set of models. A formula A is said to be C-v(Jlid iff for all models M E Sand all wE W, M, w f= A. A formula A is said to be C-s(Jtisfi(Jble iff -.A is not £-valid.

2.2 Logics in the paper

In the paper we shall consider numerous logics that ad­ mit interactions between the modal operators:

1. K1 = (For, S) is the logic such that S is the set of all the models. The K1-satisfiability problem is PSPACE-complete (see e.g. [Fagin et (Jl., HHJ5]).
2. C([R], [-R]) = (For, S) (see e.g. [Goranko, 1990a]) is the logic such that I = {1, 2} and M = (W, R1, R2, V) E S iff R1 = W x W \ R2 . The satis­ fiability problem is decidable and EXPTIME-hard [Spaan, 1993]. Similar modal logics are considered in the context of knowledge representation and rea­ soning (see e.g. [Lakemeyer, 1993]).
3. C([f]) =(For, S) (see e.g. [Segerberg, 1981]) is the logic such that I= {1} and M = (W, R1 , V) E S iff R1 = difw. The C([f])-satisfiability problem is NP-complete when Foro is infinite and in P other­ wise (see e.g. [Spaan, 1993; Demri, 1996]) .
4. I<I([f]) = (For, S) is the logic such that 1 E I (a distinguished element of I), card(!) 2: 2 and M = (W, (R;);ei, V) E S iff R1 = difw . Axiomati­ zat.ion of I<I([f]) has been studied in [Rijke, 1993; Balbiani, 1997]. For I = {1, 2}, the KI{[f])­ sat.isfiabilit.y problem is decidable and EXPTIME­ complet.e [R.ijke, 1993].

The models for C([R], [-R]) satisfy(*) R1 = W x W\ R2 . If we require(**) R1 = difw then [2]A <=>A is valid in this new logic. C([f]) can be seen as C([R], [-R]) except that the models satisfy (*) and (**) and only [1] is in the language. Moreover, KI([f]) is obtained from C([f]) by adding the operators {[i] : i E I\ {1}} that. behave as in I<1. The notion of complementary relations is therefore crucial in the semantics of the logics.

It is not the purpose of this section to recall all the features of the expressive power of the abovemen­ tioned logics (see e.g. [Goranko, 1990a; Koymans, 1992; R.ijke, 1993]). By way of example we consider the logic I<I([f]) with I= {1, 2}. As usual, a class :F of frames (W, R1, R2) is said to be KI([f])-defin(Jble iff there exists a KI([f])-formulaA such that. for all frames (W, R1 , R2), (W, R1, R2) E :F iff (W, R1, R2) f= A (i .e. for all valu­ ations V and all w E W, (W, R1 , R2 , V), w f= A). A similar notion of definability can be naturally defined for other logics.

Fact 2.1. [Goranko, 1990b; Koymans, 1992]

• All universal first-order conditions on R, = are I< I ( [ f ])-definable.
• Every finite cardinality is £([#])-definable.
• Each universal first-order formula on R is C([R], [-R])-definable.

The statements of Fact 2.1 do not hold for the logic I<1: for example the class of irrefl.exive frames is not /( 1-definable.

3 Tableaux for K1

The calculus defined for !{1 in this section can be eas­ ily obtained from existing ones in the literature (see e.g. [Fitting, 198:~]) but it will be the opportunity to intro­ duce various definitions smoothly.

We shall define prefixed tableaux following the methodology described in [Fitting, 1983]. We make sub­ st.antial use of the uniform notation for modal formulae defined in [Fitting, 1983]. Four types of formulae are usually distinguished: v (necessity), 1r (possibility), n (conjunction) and {3 (disjunction). For i E I, we intro­ duce the types vi and 1ri . For instance, --.(i)A and [i]A are of type vi ( vi 1 denotes the formulae -.A and A respec­ tively) and --. [ i] A and ( i) A are of type 1ri ( 1rf 1 denotes the formulae -.A and A respectively) .

A prefixed formula is a triple of the form cr : A [C] where cr is a pr·ejiJ:, i.e. cr is a finite sequence of natural numbers possibly superscripted by some i E J, A is a formula and Cis a couple (C1 , C2) . Each C; is a set of pairs of prefixes. When the context is clear we omit cr or [C]. The condition C is the current information on the branch

if 11' 1 is already on the branch and for some k E w, 17 1 = uki.

Figure 1: Tableaux system for 1<1

that is stored during its development. At each step of the development of a branch, C is identical for all the prefixed formulae on that branch, i.e. C is an at.t.ribute for branches. We refer to a prefixed formula a.<; atomic if it is of the form u : p [C] or u : ·JI [C] when 11 is an atomic formula. Figure 1 presents the prefixed tableau system for the logic 1<1 . Observe that the condition [C] is of no use in this calculus.

In the sequel we omit the presentution of the n-rnle (decomposition of conjunctions) and the /3-rnle (decom­ position of disjunctions) but these rules are included in any forthcoming calculus . A branch is closed if it. con­ tains contradictory prefixed formulae (for any formnla A, u : A and u : ·A are contradictory) . A tableau is closed if every branch is closed. A formula A is said to have cJ closed tCJbleau iff there is a closed tableau which root is 0 : ...,A [(0, 0)]. Termination occurs when no op­ eration is possible. A branch is open if it is not closed and a tableau is open if at least one branch is such.

Theorem 3.1. A formula A is l<J-valid iff A has a closed tableau built with the rules presented in Figure 1. The proof of Theorem 3.1 can be easily obtained from existing ones from the literature [Fit.t.ing, 198;{].

4 Tableaux for £([R], [-R])

Instead of defining a sound and complete calculns for the logic C([R], [-R]) we define a sound and complete calculus for the logic K1 2 (I= {1,2}) characterized by the models (W, R1, R2, V) where R1 U R2 = W X W (we do not require R1 n R2 = 0). It is known that. C([R], [-R]) and K1 2 have the same class of valid for­ mulae [Goranko, 199,0a] and we shall provide a decision procedure for the set of 1<1 2 -valid formulae ba.<;ed on our tableaux approach. Act.ttally from the calculns for K1 2 the careful reader will observe that a calculus for C((R], [-R]) can be easily defined. However the caknlns for K~ 2 is more adequate to define a decision procedme. The rules for the logic K~ 2 are those in Figure 2 when~

• C' = (C1 u {(u,u')},C2), C" = (C1,C2 u {(u,u 1 )}),
• C 1 " = (C1 U{(u,u')},C2U{(u, u')}).

if C; ( ( 17, 17 1 ), C) holds and 17 1 already occurs on t.he branch.

if there is no 17 1 such that. 17 1 : 1r~ on the branch and either C;( (17, u'), C) m· (for all u :vi on t.he branch, u' : v~ is on the branch).

17,17 1 not. already applied with this rule

Figure 2: Tableaux system for 1<~ 2

For the logic /(~2 , C;((u,u'),C) holds (i E {1,2}) iff ei­ ther (u, u') E C; or u' = uk; for some k E w. Intuitively, C; encodes the accessibility relation R;. The condition C could be deleted in the definition of the calculus since it only stores some information about the way the rules have been applied on the branch. However, if one wishes to implement our calculi, the actual presentation is well­ suited for this purpose. For instance the vi-rule can be read as follows. If the formula u : vi occurs on the branch and if the current. information on the branch is C then add u' : vf1 on the branch and C remains un­ changed. It is worth observing that. the cut. rule cannot be deleted unless completeness is lost.. This property is also shared by the cut rule in the calculi defined in [d' Agostino, HHJ~~]. It is also worth noting that the con­ dition of the restricted cut rule in Figure 2 is equivalent. to: either not. C1((u,u'),C) or not C2((u,u'),C). More­ over, by applying the restricted cut. rule, the current in­ formation C on the branch is updated.

4.1 Soundness

Let. X be a set. of prefixed formulae having the same con­ dition C (what. happens at a current stage of the devel­ opment. of a given branch) . Let. M = (W, R1 , R2 , V) be a K1 :.~-model. By an interpr·etcJtion of X in M we mean a m~pping I : { u : u : A E X} ~ W such that if u, 11' 1 occm in X , then C;((u,u'),C) implies (I(u),I(u')) E R; (i = 1, 2). We say that X is K1 2 -sCJti8jiCJble under the interpr·etution I if for each u : A E X, M,'I(u) f= A. We say that X is K1 2 -sat.isfiable if X is 1<1 2 -satisfiable under some interpretation. We say that. a 'branch of a tableau is [(~ 2 -sCJtisfiuble if the set of prefixed formulae on it is K1 2 -sat.isfiable. A tableau is 1<1 2 -sCJti.sfiCJble if some branch is. '

Lemma 4.1. Suppose T is a prefixed tableau that. is K1 2 -satisfiable. Let. T' be the tableau that. results from a single t.ablean rule being applied to T. Then T' is also [( ~ 2 -sa.t.isfiable.

Proof: By an easy verification. Q.E.D.

Proposition 4.2. (soundness) If A has a closed tableau built with the rules in Figure 2 then A is 1<~ 2 -valid.

Proof: Similar to the proof of Theorem 3.2 in [Fitting, 1983] (p.400). Q.E.D.

4.2 Completeness

Let A be a formula. As done in [Fitting, 1983], we de­ fine a systematic attempt. to produce a proof of A. The procedure is in stages and the stage 1 consists in plac­ ing 0 : -,A ((0, 0)] at the root. Now suppose n stages of the construction have been done. If the tableau is closed then we stop. Similarly if every occurrence of a pre­ fixed formula is finished (see the definition of 'finished' below) then we stop. Otherwise we go on. If n + 1 is even, u, u 1 satisfies the condition of the cut rule on some open branch BR (chosen in some f(lir· way) and (u, u 1 ) is the smallest pair (for some encoding in the set of nat­ ural numbers w) satisfying this property then split the end of branch BR in three sub-branches by applying the restricted cut. rule with (u, u 1 ). Otherwise (n + 1 odd) any stage n + 1 consists in choosing an occurrence of a prefixed formula u : B [C] as high up in the tree as possible (as close to the origin as possible) that has not been finished. If o- : B [C] is atomic then the occurrence is declared finished . This ends the stage n + 1 otherwise we extend the tableau as follows . For each open branch BR through the occurrence of (1 : B [C] (under· the pmviso the conditions to apply the rules hold) :

• P1 If (1 : B [C] is of the form o- : a [C] add (1 : n 1 [C] and o- : a2 (C] to the end of BR.
• P2 If o- : B [C] is of the form (1 : f3 [C] split the end of BR and add o- : {31 (C] to the end of one 8ub-lmmch and o- : fJ2 (C] to the end of the other one.
• P3 If (1 : B [C] is of the form (1 : vi (C] then for all (1 1 satisfying the condition of the vi-rule add (1 1 : v/ 1 (C] to the end of BR, after which add a fresh occurrence of o- : vi (C] to the end of BR.
• P4 If o- : B [C] is of the form (1 : 11'i (C] then add (Tki : 11'1 1 (C] to the end of BR. Moreover for (1 : vi (C] on the branch add (Tki : v/ 1 (C] to the end of BR (applications of the vi-rule)

Having done this for each branch BR through the par­ ticular occurrence of o- : B [C] being considered, declare that occurrence of (1 : B [C] finished. This ends stage n + 1.

Definition 4.1. Let X be a set of prefixed formulae and C be a condition. We say X is downward-8atumted with respect to C iff:

• C1 For all o-,o- 1 E X, (Cl.1) either C1(((1,(1 1 ),C) or C2( (o-, (1 1 ), C) and, (Cl.2) for all p E Foro, { (1 : p, (1 1 : ..,p} ~ X implies o- :f:. (1 1 ·
• C4 if (1 : vi E X then for all (1 1 in X satisfying the condition of the vi-rule, we have (1 1 : v{, EX.
• C5 if (1 : 11'i E X then there is (1 1 such that (1 1 : 11'[ 1 E X and, either C1(((1,(1 1 ),C) or (for all o-: viE X, (1 1 : IJ:, EX) .

C2 if o- : a EX then {o-: a 1, o-: a2} ~X.

• C3 if o- : f3 E X then either (1 : /31 E X or (1 : /h E X.

Lemma 4.3. If X is downward-saturated with respect to C then X is 1<~ 2 -satisfiable .

Proof: Assume X is downward-saturated wrt. C. Let. M = (W, R1, R2, V) be the structure such that W = {(1 : (1 : BE X}, for all p E Foro V(p) = {o-: o-: p EX} and for all (1, (1 1 in X and i E { 1, 2} o-Rio- 1 iff either Ci(((T, (1 1 ), C) or {v{, : o- : vi EX} ~ {B : (1 1 : B EX}. One can easily check that the definition of M is correct, i .e. M is a 1<~ 2 -model. It can be shown by induction on the structure of the formulae that for every formula B and every prefix o-, if (1 : B E X then M, (1 I= B (and therefore X is 1<~ 2 -satisfiable). Q.E.D.

Proposition 4.4. (completeness) If A is I<1 2 -valid then A has a closed tableau built. with the rules pre­ sented in Figure 2.

Proof: Suppose A has no closed prefixed tableau. So the systematic procedure does not. generate a closed tableau. We build a tableau with this procedure by considering 0 : -,A ((0, 0)] at the root. If the procedure termi­ nates then the tableau contains a non-closed branch. If the procechue does not terminate, by Konig's Lemma, there is an infinite non-closed branch . The systematic procedure guarantees that the non-closed branch BR is downward-saturated wrt some C. By Lemma 4.3, BR is K1 2 -satisfiable. Since 0 : -,A E BR, there is a K1 2 -model M'and a world w such that M, w I= -,A, which, leads to a contradiction. Q.E.D.

In the systematic procedure, we require that if (1 : B is a conclusion of some inference of the vi-rule and if an occurrence of (1 : B has already been introduced on the branch then no new occurrence is added on the branch. The systematic procedure still guarantees completeness but it terminates since the 11'i-rule can be applied only a finite number of times. Actually, each 71'i-rule is applied at most mwi(A) X 2c"rd({B,-.B:B $Ubformul" of A}) times on a branch where mwi(A) is the number modal opera­ tors of the form ( i] or ( i) occurring in A . The other rules do not introduce new prefixes which guarantees termi­ nation since their applications are restricted (while in­ suring completeness). The systematic procedure above is therefore a decision procedure for the .C([R], (-R])­ validity problem.

5 Tableaux for £([~])

For any finite set X of pairs we write X(a, b) to denote that (a, b) belongs to the smallest equivalence relation containing X . The rules for .C((:f:.]) are those for K~2

except. that. the 1r 1 -rule becomes

u : 1!"1 [C] 1 . 1 [( {( 1)})] new k E w on the bnmch uk . 1l"o c1, c2 u u, uk

and the restricted cut. rule is replaced by:

u,u' occur on the branch and neither C1((u,u'),C) nor C2((u, u'), C) holds.

The definitions of C1 and C2 are modified as follows : c1((u,u'),C) holds iff either C1(u,u') holds or u = u' and c2 ( ( u, u'), C) holds iff there exist u1 and u~ such that {(u1,ul.),(u~,u1)} n C2 # 0, C1((u,u1),C) and cl((u',ul.),C). For instance cl((u,u1),C) can be inter­ preted by "u and u1 are equal modulo C". A branch is closed if there exist prefixed formulae u : A and u' : -.A on that branch such that Cl((u,u'),C) holds . This cal­ culus for £([#]) strongly differs from the one in [Demri, 1996] due to the machinery associated to C and to the restricted cut rule.

Theorem 5.1. (soundness and completeness) A for­ mula A is £([#])-valid iff A has a closed tableau built with the rules for£([#]) .

In order to provide a decision procedure for£([#]) it is sufficient to consider the decision procedure in Section 4 adequately modified for£([#]) except that the following conditions are required to apply the 1r 1 -rule:

• p1 it is not possible to apply the restricted cut rule (that is the restricted cut. rule is S(Jtumtt:rl before applying the 1r 1 -rule),
• p2 there is no u' : 1!"~ on the branch such that C2( (u, u'), C),
• p3 there are no u1 : 1!"~ and u2 : 1r{, on the branch such that C2 ( ( u1, u2), C).

It is possible to show that the calculus is sound and com­ plete and the systematic procedure defined above always terminates (each formula 1r 1 occurring in -.A can be used at most twice as a premise of a 1r 1 -rule inference on a given branch) . Actually, at most 1 + 2 x mw(A} differ­ ent prefixes can occur on a given branch where mw(A) is the so-called modCJl weight of A, i.e. the number of modal operators occurring in A. Hence the above sys­ tematic procedure constructs a polynomial-size £([#])­ model for -.A (with respect to the size of A} if A is not £([#])-valid.

6 Tableaux for KI([#])

The conditions C1 and C2 are defined as in Section 5 as well as the closure conditions. The tableaux rules for K1 ([-:f]) are given in Figure 3. Let X be a set of prefixed formulae having the same condition C and M = (W, (R;};Ef, V) be a KI([#]}-model. By an inter·­ pretCJtion of X in M we mean a mapping I : { u : u : A E X} -t W such that. if u, u' occur in X, then

• u' = uk' for some k' implies (I(u),I(u')) E R;,

if t.here exist. u1 ,u1 ki on t.he branch such t.hat C1((u,u1),C) and Ci((u',ulki),C).

u, u' on t.he bmnch and neither C1 ( (u, u'), C) nor C2( (u, u'), C) holds.

Figure 3: Tableaux system for KI([-:f])

• C1 ( (u, u'), C) implies I( u) = I( u') and C2 ( (u, u'), C) implies I(lT) -:f I(lT 1 ).

Lemma 4.1 can be shown to hold for KI([-:f]) associ­ ated with the calculus presented in Figure 3: if A has a closed tablean built with the rules in Figure 3 then A is KI([#]}-valid. We also use the systematic procedure de­ fined in Section 4.2 (with the binary restricted cut. rule) except that (P4} is replaced by:

• P4' If lT : B [Cl is of the form u : 1!"; [C] with i -:f 1 (resp. lT : 1r [C]} then add uk' : 1r!1 [C] (resp. uP : 1r~ [(C1,C2 U {(lT,lTk1)})]} to the end ofBR.

Similarly, we say X is downwCJrd-s(Jtumted uiT't C iff:

• Cl' For all lT,lT 1 E X, (C1'.1} C1((u,u'),C) iff not c2 ((lT,lT 1 ),C) (note the difference with Cl.1 in Sec­ tion 4} and, (C1'.2} for all p E For0 , {u : p, lT 1 : -.p} ~ X implies c2 ( (lT, lT'), C) .
• Conditions C2,C3 from Section 4.2 and C4 fori -:f 1
• C5' if lT : 1r 1 E X with i -:f 1 then there exist lT 1 : 11"11 E X and lTk 1 in X such that C1((lT 1 ,lTk 1 ),C) .
• Cti if lT : l/ 1 E X then for all u' in X such that C2 ((lT,lT 1 ),C), we have lT 1 : vc~ EX
• C7 if lT : 1r 1 E X then there is u' such that. lT 1 : 1r{, E X and C2 ((lT,lT 1 ),C).

Lemma G.l . If X is downward-saturated wrt C then X is I< 1 ( [ -:f] }-satisfiable.

Proof: Assnme X is downward-saturated wrt C. Let M = (W, (R;) ;ei, V) be the structure such that,

• W = {llTI : lT :BE X} where llTI = {lT' : lT: BE X,c1((lT,lT'),C)}.
• for aliT' E Foro V(p) = {lui : u: p EX}.
• R1 = difw and for all u, u' in X, luiR;IlT'I (i # 1} iff 3lT1, lTtk' in X, C1((lT, u1), C) and C1((lT', lT1k 1 ) , C) .

M is a KI([:f])-model. It. can be shown (by induction on B) that if <T: BE X then M, I<TI f= B . Q.E.D.

Proposition 6.2 . (completeness) If A is KI([:f])-valid then A has a closed prefixed tableau built with the rules presented in Figure 3.

In order to obtain a decision procedure, take the system­ atic procedure, incorporate the restrictions p1, p2 and p3 from Section 5 and for i :f 1, add the following restric­ tion to the 1r;-rule: there is no <T 1 : 1r~ on the branch such that C1 ( (<Tk;, <T'), C) holds for some k E w .

7 Concluding remarks

The use of prefixes for tableaux systems dedicated to modal logics has been thoroughly developed in [Fit­ ting, 1983] whereas our treatment of the condition C (see e.g. Sections 4, 5, 6) can be viewed as a means to parametrize our calculi by the theory of the acces­ sibility relations. Hence, the idea of theor·y resolution [Stickel , 1985] in which a theory is separately dealt with from the rest of the calculus is present in our calculi. This idea is not new in the realm of the mechaniza­ tion of modal logics (see e.g. [Frisch and Scher! , 1990; Gent, 1993]) but the originality of our work is related to the conditions satisfied by the accessibility rdations of the models.

The second important feature of our calculi is the use of a restricted cut rule. Recently, various works have t(lmed the cut rule for calculi dedicated to modal logics (see e.g. [d'Agostino, 1993; Governatori, 1995]). How­ ever our calculi do not have a cut rule with a branching for formulae . In that sense, the cut rule in our calculi is even more restricted than the one in [Governatori, 1995].

We have defined sound and complete prefixed tableaux calculi for the logics .C ( [ R], [-R]), and I< 1 ( [ :f]) (also for K1 and .C([:f])) and decision procedures have been de­ signed from these systems. It. is worth noting that the expressive power of the modal logics with enriched lan­ guages is attractive in the Artificial Intelligence commu­ nity since for instance the operator [#] has already been shown to be useful to reason about time [Sain, 1988; Koymans, 1992] or space [Balbiani et al., 1997].

Future work could be oriented towards the inr.orpora­ tion of our calculi into existing tableaux-based theorem provers for modal logics and towards the definition of other prefixed tableaux for modal logics with enriched languages including for instance, the logics in the paper where standard conditions for the accessibility relations are required -reflexivity, symmetry, ....

Acknowledgments: the authors thank Luis Farinas del Cerro for his encouragements.