Matrix Proof Methods for Modal Logics

1 Introduction.

Modal logieo are widely ued in varioue branchee of artificial intel­ ligence and computer ecience u logice of knowledge and belief ( eg., [Moo80,HM85,Kon84]}, logieo ofprograme (eg., [Pne77]), and for epec­ ifying distributed and concurrent ayateme ( eg., [HM84,Sti85b]). Aa a consequence, the need ariaee for proof eyatema for theee logics which facilitate efficient automated proof eearch.

Traditional proof oyateme for modal logica, such u tableau- or sequent-baaed eyateme are readily available (eg., [Kan57,Nia8S,Fit8S]). While theee eyateme are to aome extent human-oriented, the proof rules form an inadequate buia for automated proof eearch since they generate search apacee that contain conaiderable redundanciea. The redundanciee arise mainly from the characteriatic emphuia on connec­ tives and the proof rulee for modal operaton and quantifiera.

The matrix methoda for firat-order cluaical logic, pioneered by Prawite [Pra60], and further developed by Andrews [And81] and Bibel [Bib81], have been demonstrated to be·leu redundant than the moat efficient of the resolution baaed methoda for that logic [Bib82b]. The methode combine an emphuia on coruaection~ (drawn from the reso­ lution methoda) with an intensional notion of a poth.

In thia paper we preeent matrix proof ayateme for the modal log­ ieo K, K4, D, D4, T, 84 and 85, baaed on modal veraione of Bibel'a ·computationally improved" Herbrand Theorem for firat-order cluai­ cal logic [Bib82c]. We consider both conatant- and varying-domain versions of the firat-order modal logica.

The major featuree of oar approach may be aummarieed u follows. Validity within a logic ia characterised by the exiatence of a aet of connections (paira of atomic formula occurrencea: one positive, one negative) within the formula, with the property that every eo-called atomic path through the formula contains (u a aubpath) a connec­ tion from the set (§ 2.4). Such a aet of connections ia aaid to span the formula. For cluaical propositional logic thia condition auflices [And81,Bib81]. For firat-order logic a substitution (of parametera or terms for variables) mUit be found under which the (then proposi­ tional) connections in the epanning eet are aimultaneoUily complemen­ tary. Conditione are placed on the eubatitution that ensure amongst

: Thio work wu oupportad In part by SERC p-ant GR/D/4.4874

MATRIX PROOF METHODS FOR MODAL LOGICS

Lincoln A. Wallen

University of Edinburgh, Scotland

other things that a proof within a particular tableau- or aequent-bued proof eyatem ia conatructable from the connections and the aubati­ tution [Bib82c,Wal86]. This buically amounte to ensuring that the restrictions found on the traditional quantifier rulee can be met.

For the propositional modallogice we keep the buic matrix frame­ work but define a notion of complementarity for atomic formulae that enaurea the exiatence of a proof in one of Fittin1'· prefiscd tableau eyateme [Fit72,Fit8S]. Thia amounte to ensuring that, eemantically: the two atomic formulae of a connection can be interpreted u inhabit­ ing the same "poaaible world, · and proof-theoretically: that they can be given the same prefix (§ 2.5.1). The key obeervation ia that thia can be established by noting the position of the atome relative to the modal operatora in the original formula and utilising a epecialieed uni­ fication algorithm operating over repreeentations of these positions. Clearly, thia notion of complementarity ia logic-dependent, a depen­ dence which ia reflected in the choice of unification algorithm. Lifting theee reeulte to firat-order constant-domain modal logica ia aimply a matter of combining thia modal notion of complementarity with the firat-order notion (§ 2.5.2).

For the. varying-domain veraions we index individual variablea with the prefix of their quantifier. The aubatitution of one variable for another ia permitted provided their prefixea can be unified (§ 2.5.2).

Checking a formula for validity within a modal logic ia therefore reduced to a proceu of path checlr.ing and complementarity teate per­ formed by a apecialiaed unification algorithm(§ S). Daring thia proceu extra copiea may need to be considered of univeraally quantified for­ mulae and/or formulae dominated by a modal operator of ·neceuary· ( 0) force. The duplication in both cuee ia managed by an extension of Bibel'a indexing technique or maltipllcitr [Bib82a] which aupporta the implementation of the matrix eyateme Uling atructare-aharing tech­ niques [BM72]. The notions of multiplicity, aubatitu&ion and apanning seta of connections form the buia of the relationship with Herbrand'a Theorem.

A number of authora haw attempted to adapt computationally oriented proof eyateme for firat-order logic to the modal logica con­ sidered here (eg., [Far8S,AM86a,Kon86]). We compare oar approach favourably to theira in Section 4.

2 The modal matrix 11JIItema.

2.1 Prellmlnarl·.

We uaume familiarity with the uaual definition of the modallan1uage and formulae. We let A, B range over formulae and P, Q range over atomic formulae.

A pair (G, R), compriaing a non-empty eet G and a binary relation R on G ia called a frame. Let D be aome non-empty aet. A fir.t-order /NJme over D ia a triple (G, R, P) where (G, R) ia a frame and P ia a mapping from G to non-empty aubaete of D. P(w) can be interpreted u the eet of individuals that "exiat" in the world w.

We can obtain different veraione of the firat-order logics by re­ stricting the way in which P variee from world to world. For ex­ ample, we could require the coruta.r~t-doma.i11 condition: for w, w' E G, P(w) = P(w'). Axiomatically, constant-domain modallogice are ob­ tained by including the so-called Barcan formula Vz 0 Az => 0 VzA.z as an additional axiom. Our purpose here is not to choose between these possibilities but to develop matrix proof systems for each of the variants.

If we restrict R to satisfy the conditions outlined in Table 1, we say that {G,R,P} is an !-frame over D, where .Cis the logic associated with the conditions. The "idealization" condition is that for every element wE G there is some element w' E G such that w R w'. Once again our purpose is not to choose between these logics but to develop matrix proof systems for each.

An .C.-model over Dis a pair ((G,R,P},If-} where (G,R,P) is an !-frame over D and If- is a relation between elements of G and sentences such that: for all w E G

1. w If- A 1\ B iff w II- A and w II- B . 2. w If- A VB iff either w If- A or w If- B . 3. w If- A~ B iff either wllfA or w If- B. 4. w II- -,A iff w I if A. 5. w If- 0 A iff for all t1 E G with w R tt, t1 If- A. 6. w If- <)A iff for some t1 E G with w R v, t1 If- A. 7. w If- "v'xA iff for all dE P(w), w II- A[d/x]. 8. w If- 3xA iff for some dE P(w), w II- A[d/x].

Satisfaction in a model and validity are defined as usual.

A aigned formula is a pair (A, n) where A is a formula and n E { 0,1 }. We let X, Y range over signed formulae. Informally, the signs "1" and ·o· should be interpreted as the qualifiers "is true· and "is false" respectively. For ease of exposition we use a uniform notation due to Smullyan and Fitting that classifies signed formulae according to their sign and major connective/operator as shown in Table 2.

2.2 Formula occurrences.

A formula. tree for a signed formula is a variant of its formation tree containing additional information as to the polarity of its subformula occurrences (i.e., whether an occurrence of a subformula is negative or positive within the formula). It is best explained by example. A formula tree for the signed formula is shown in Figure 1. Following Bibel [Bib82c], we name the nodes or poaitiona of the tree (a0-a14) so as to distinguish different occurrences of the same subformula. With each position we associate the polarity of the subformula rooted at. that position and a label consisting of the major connective/operator of that subformula, or the subformula itself when that is atomic. We use < to denote the (partial) ordering in the formula tree. Positions form the basis for implementations of the matrix systems using structure-sharing techniques [BM72]. A position should be interpreted as a pointer to a single copy of the main formula stored in computer memory. Unlike resolution-based methods, these matrix methods do not require the explicit generation of intermediate formulae.

In terms of analytic tableau systems [Smu68,Fit83], the polarity of a position determines the sign with which the subformula rooted at that position will occur on any analytic tableau which has the main (signed) formula as root [Wal86]. Therefore, the classification of signed formulae can be extended to the positions of a formula tree by defining the type of a position to be the type of the signed formula rooted at that position in the tree. In addition, we consider the root node of the formula tree to be of 1r0 type.

Notice that each position has two types: its principal type (eg., a, p, v, .. . ) is determined by its label and polarity, while ita secondary type (eg., a<~o 0<2, P1, .. . ) arises from the type of its parent.

For a given formula tree we use k,l, poaaibly subscripted, to denote positions and llo, no, r 0 and .O.o to denote the sets of positions of type vo, ~ro, 'Yo and 5o respectively.

2.3 Multiplicities.

The semantic clauses for interpreting formulae whose major symbol is a modal operator of "necessary· force (i.e., v-type) or a quantifier of ·universal" force (i.e., "'-type) indicate that we must consider multiple instances of the principle subformula of such a formula occurrence (i.e., formulae rooted at v0- and 'Yo-type positions respectively within a formula tree) . In the modal cue we intend different instances to inhabit different worlds; in the case of a quantified formula, we form different instances by the substitition of different parameters for the (universally) bound variable.

The following definitions are introduced for a given formula tree for a. given signed formula X .

A function JAM from 1.10 to the positive integers is called a modal multiplicity for X; it serves to encode the number of instances of sub­ formulae of X in the scope of a modal operator of necessary force considered within a putative proof.

A function p.q from r 0 to the positive integers is called a firat­ order multiplicity for X; it serves to encode the number of instances of subformulae of X in the scope of a quantifier of universal force considered within a putative proof.

A multiplicitv P.. for X is the combination of a modal and first-order multiplicity thWI: for a position k of the formula tree

H p. is a multiplicity for X we define the (indexed) formula tree for the inde:z:ed formula X~' as a tree of indexed positions of the form k", where k is a position of the basic formula tree for X and K. is a sequence of positive integers defined as follows: if k1 < k2 < · · · < k,. :$ k, 1 :$ n, are those vo- and "to-type positions that dominate k in the basic formula tree for X, then

The ordering in the indexed tree <" is defined in terms of the ordering on the underlying tree: for indexed positions k" and 1·

where 8 is some sequence of positive integers. The polarity and label of an indexed position k" is taken to be the same as the polarity and label of its underlying position k except that, in the cue of atomic formulae, individual variables are indexed with the index of the child of their quantifier position (i.e., a "'o or 60 position) so as to distinguish the different instances. Consequently, indexed positions inherit the type of their underlying position also.

Figure 2 shows the indexed formula tree for the example formula of Figure 1 with a multiplicity of p.q(a4) = 2 and constant (i.e., 1) otherwise. As a convention we omit indices consisting of the empty sequence.

We let u, v, possibly subscripted, range over indexed positions when we are not interested in the index, and drop the superscript on <. We abuse our notation and let l-fl, II0 etc, denote the sets of indexed posi­ tions of an indexed formula tree of the appropriate types. Henceforth we shall refer to indexed positions simply as positions.

Remark. Bibel's notion of a multiplicity [Bib82aJ corresponds to our notion of a first-order multiplicity. We have altered his definition slightly to support the symmetry between the treatment of modal op­ erators and quantifiers obtained above. Notice that, for an indexed formula, the set r 0 and the set of distinct universally quantified vari­ ables, and the set .O.o and the set of distinct existentially quantified variables in the .formula are in 1-1 correspondence. We shall make use of this observation in the sequel. ·

2.· Patha and connections.

Let X" be an indexed formula. A path. through X" is a subset of the positions of ita formula tree defined below. We shall use s, t, possibly subscripted, to denote paths, and adopt the notation s[a"J to denote a path s with an occurrence of a distinguished a-type position with index te. Similarly for the other types. The set of paths through X", is the smallest set such that:

1. { k~) } is a path, where ko 0 is the root position of the formula tree for X~';

The path (s- {a"}) U {a1",a2"} is said to have been obtained by reduction on a" from s[a"J. Similarly in the other cases.

Each path s through X determines a set (branch or aequent) of positions as follows

A path, a, through X" is an atomic path iff fork" E a, either

• (a) k is labelled by an atomic formula; or
• (b) k Ell, and for all;, 1 :$; :$ P.M(vo), vo"; E S(s); or

Remark. Our definition of path differs from Andrews' [And81J and Bibel's [Bib81J definition so as to demonstrate the relationship between the matrix methods and tableau/sequent methods. Each clause in the definition, when interpreted as operating on the branch associated with the path, corresponds to an analytic tableau rule [Smu68,Fit83J. A path is a representation of the unuaed formulae on a branch. Further­ more, for a given multiplicity, the branch associated with an atomic path is complete. These relationships are discussed in more detail in [Wal86]. ·

Consider our example (signed) formula indexed as in Figure 2. H we distinguish its a-type subformulae from its ,8-type subformulae by placing the components of the former side-by-side and the components of the latter one above the other, we obtain a nested matrU: thus:

Notice that the two instances of the subformula P:t/\Qo; are considered to be the components of an implicit a-type formula. This follows from the '1 clause (6) of the definition of paths above. H we omit the connectives and operators we are left with the skeleton matrix:

which corresponds in part to the so-called "deep formula" in the ex­ pansion tree approach of Miller [Mil84] .

The atomic elements of an atomic path are simply the horiaontal matrix paths through such a matrix. In this case there are two atomic paths through the formula, one with atomic elements {Po;! 1 l, Qo;! 1l, P:t(2), Qo;!2), Py(l)} and one whose atomic elements are {Po;(l) ,Q:z:(l), P:z:( 2 ), Q:z:(2), Qz(1l}. More precisely, we should express these sets as positions thus: {a~ 1 l, a~ 1 l , a~ 2 l, a1 2 l, a~~} and {a~ 1 l , a~ 1 l, a~ 2 l, a~ 2 l, a~h

A connection in an (indexed) formula is a subpath of a path through the formula consisting of two positions labelled by an atomic formula with the same predicate symbol but of different polarities. A set of connections is said to 1pan the formula just when every atomic path through it contains a connection from the set.

For example, the two connections { a~ 1 ), a~~} and { a~ 1 ), a~~} span the indexed formula displayed above. So does the connection pair {a~ 1 ), a~~} and {a~ 3 ), a~~}.

2.5 Complementarity.

As remarked above, for a given multiplicity, the atomic paths through an indexed formula serve to represent the branches of a complete an· alytic tableau with the main formula at its root. In the same spirit, we wish to interpret connections as the two formula occurrences that atomically close the branches on which they occur.

For propositional logic, connections are complementary by defini· tion. Since there ia no need for multiplicities {no modal operators or quantifiers) this observation leads to a simple characterisation of validity.

Theorem 2.5.1 ( Andrewa,Bibel) A propo1itional formula A i1 vlllid iff there uilt1 a 1et of connection· that 1pan1 (A, 0) .

This theorem ia the matrix counterpart to the following theorem for analytic tableaux:

Theorem 2.5.2 (Smullyan) A propoaitional formula A ia valid iff there e:Ntl an atomically clo1ed anlllvtic tableau for (A, 0).

The matrix theorem is more appropriate as a baais for automated proof search because there is no need to actually construct a tableau. The spanning condition simply ensures that a tableau of the appro­ priate form can be constructed; we search for a spanning set of con· nectiona directly rather than via the connective oriented tableau rules [Wal86].

In the presence of modal operators and quantifiers we must be more careful We deal with modal operators first .

2.5.1 Propositional modal syatems.

Informally we must ensure that the two atomic formulae represented by the positions of a connection can be considered to inhabit the aame possible world. In terms of tableaux, this involves synchronising the choices of possible worlds made during the reduction of the modal (eub)formulae that contain these atomic formulae aa subformulae; or, in terms of positions, the reduction of the v- and lr-type positions that dominate the positions of the connection in the formula tree.

The following definitions are introduced for a given (indexed) for· mula tree for a given {indexed) formula X~' .

Let Tu denote the union of llo and Il0 · We aasociate a sequence of positions called a pre/is, denoted pre{u), with each position u of the formula tree as follows: if u1 < u3 < · · · < u,. :$ u, 1 :$ n, are those Tu-elementa that dominate u in the formula tree, then

The prefix of a position encodes its modal context within the formula tree. We shall use p, q to denote prefixes.

For example, the prefix of a~ 1 ) is ( a0a3a3a~ 1 )) while the prefix of (1) · ( (1)) a 13 18 aoa 10 ·

We can place various conditions on a binary relation Ro s;; TM xTu as shown in Table S. Such a relation is an .C·acce11ibility relation provided it satisfies the properties usociated with .C in Table 4.

Remark. These definitions are adapted from Fitting [Fit72,Fit83]. Each prefix ·names· a possible world. Since the positions of the {in­ dexed) formula tree correspond to signed subformulae of X~', a position taken together with its prefix corresponds to his notion of a prefised signed (eub)formula. The prefix identifies the world in which the sub­ formula ia taken to. be true or false depending on ita sign. Binary relatione on prefixes are thus used to represent the properties of the acceuibility relation for a given logic. ·

We have indicated that the two positions that constitute a connec­ tion must be interpreted aa inhabiting the same pouible world; i.e., have the same prefix. We ensure thia by building a modlll 111ob.titu· tion aM under which the prefixes of the positions are identical The discussion below motivates the ensuing definitions.

Consider a v-type position u with prefix p. The semantic clause for the subformula rooted at u allows us to conclude that the subformula rooted at the child of u, say v, has the same truth value {sign) in an11 world acceuible from the world denoted by p. By definition, the prefix of " is (pv) since t1 is of v0-type. Tables S and 4 give us the conditions under which a prefix can be considered to be acceuible from p.

Take D4 for example. Any prefix of which p is a proper initial subsequence will be acceuible from p. Consequently, if we consider t1 to be a ·variable" and allow it to be instantiated under some map­ ping aM: llo-+ Tu to any non-empty sequence we can guarantee that the image of (pv) under {the homomorphic extension of) au will be acceuible from the image of p under (the homomorphic extension of) aM. In the cue of 54, we allow t1 to be instantiated with any sequence including the empty sequence to reflect the reflexivity of the 54 ac­ ceuibility relation. For 55, since our notion of prefix is different, we need only consider unit sequences as pouible instantiations for such "variables. ·

Now consider a lr-type position u with prefix p. The semantic clause for the subformula rooted at u allows us to conclude that the subformula rooted at the child of u, say v, has the eame truth value (sign) as u in ·ome world acceuible from the world denoted by p. Again, by· definition, the prefix of t1 is {pv) since t1 is of a lro-type. From the tables we can see that (pv) itself ia acceuible from p by virtue of the fact that acceuibility relations on prefixes for all of the logics satisfy the general condition. Consequently we consider lro-type positions as "constants· under the mappings au introduced above. In the context of a tableau proof, the choice of thia possible world must be arbitrary; i.e ., the prefix (pv) must be new to the tableau. The "constant· " can only be introduced in a prefix by the reduction of v's parent u, or by the reduction of a v-type position introducing a ·variable" {a v0-type position) whose image under aM contains v. To preserve soundneu therefore, we must ensure that the former can occur before the latter. ·

A modal substitution au: llo -+ TM induces an equivalence relation -Manda relation CM on TM x Tu as follows:

1. If aM{u) ="for some t1 of vo-type, then u -u v.
2. If aM(u) = p and pis not a unit sequence consisting of avo-type position, then for all " :::$ p, " Cu u; where :::$ ia the subsequence relation on Tu.
3. If" Cu u and u -u u', then t1 Cu u'.

A modal substitution au is .C·admil1ible provided

1. aM respects .C-acceuibility relations Ro, i.e., for all p, q E TM,

where u!: TM -+ TM is the homomorphic extension of O'M to TM.

1. (K-logics only) u -M u' implies v eM u (and hence v eM u') for some position v.
2. <l = (< U eM)+ is irreflexive, where eM is the relation induced by O'M described above.

The appropriate notion of complementarity for the propositional modal logics under consideration is as follows: (for an indexed formula X") if O'M is an £-admissible modal substitution for X" a connection { u, v} in X" is said to be O'M-complementary iff

Remarks. The relation v eM u should be interpreted as a pre­ scription that ·position v should be reduced before position u, · in the sense of tableaux. The relation <l is called the reduction ordering. Its irreflexivity ensures that we could construct an analytic tableau with X as root using the generic prefixes instantiated by u M, so that all of the restrictions on prefixes mentioned above are met. This method of representing the restrictions on traditional modal tableau rules is an adaptation of the method used by Bibel ]Bib82a] for the classical quantifier rules.

Suitable mappings can be computed using variants on a string­ unification algorithm. In all cases the set of most general unifiers is finite but not necessarily a singleton ]Sie84]. For 55 the standard unification algorithm suffices. The admissibility check is an check for acyclicity if <l is interpreted as a directed graph.

The extra condition for the K-logics is a translation into the current setting of Fitting's notion of a wed prefix. Basically, since these logics are not idealisable we must ensure that each prefix (under O'M) of a vo-type position (formula) has been introduced by the reduction of a lf-type position (formula) beforehand. ·

We have proved the following theorem:

Theorem 2.5.3 A propo·itional modal formula A io .C-valid iff there i· a modal multiplicity PM, an .C-admi .. ible modal·ub·titution O'M and a 1et of O'M-complementary connection· that ·pan· the indexed formula (A,O)"u.

The proof involves showing that starting from a tableau with (A, 0) at its root we can construct an atomically closed prefixed tableau by following the reduction ordering induced by the substitution, and pre­ fixing each subformula with the image under the substitution of the prefix of its root position. The multiplicity indicates the number of times a given v-type formula is reduced to form the tableau. Complete­ ness involves showing that a suitable modal multiplicity PM can be constructed to form a modal Hintikka set from the set associated with any non-complementary atomic path (i.e., unclosed branch) through (A,O)"u

Although we have used tableau systems to motivate the definition of the matrix systems, no tableau construction is actually performed in the use of such methods. The theorem above is utilised directly. (See Section].)

2.5.2 First-order modal systems.

Extending the propositional matrix systems presented above to first­ order modal logics is straightforward. We consider both constant- and varying-domain versions.

For constant-domains, a pair of atomic formulae labelling the po­ sitions of a connection can be interpreted as complementary if we can find a fir&t-order substitution O'Q of parameters for individual variables that render the two atoms identical.

For varying-domains, the modalities and quantifiers interact. U ni­ versally quantified variables only range over those individuala that ·ex­ ist" in the world denoted by the prefix of their quantifiers. Existential quantifiers express the existence of individuala only in the world de­ noted by their prefixes. Consequently, our first-order substitution O'Q must respect the modal substitution O'M.

Instead of introducing an explicit set of parameters we note that there is a 1-1 correspondence between r 0 and the set of distinct uni­ versally bound variables, and ~o and the set of distinct existen.tially bound variables within the indexed formula. Consequently first-order substitutions are considered over these positions rather than individ­ ual variables. Notice that the position corresponding to the individual variable :z: quantified at a position u is the child of u in the formula tree.

More formally, let TQ denote the set fo u ~o. A first-order sub­ stitution is a mapping O'Q: f 0 -+ TQ. For soundness, we must place restrictions on first-order substitutions to ensure that the positions rep­ resenting parameters introduced for existentially bound variables (~0) are indeed arbitrary. In terms of tableaux, we must ensure that such positions are introduced (by the reduction of their parent) before the introduction of any position representing a universally bound variable which receives the same parameter under the substitution O'Q. The similarity between these restrictions on quantifier reductions and the restrictions on modal operator reductions is not accidental]Smu70].

A first-order substitution O'Q: fo -+ TQ induces an equivalence relation -Q and a relation eQ on TQ x TQ as follows:

1. If O'Q(u) = v for some v of "to-type, then u -Q v.
2. If O'Q(u) = v for some v of Oo-type, then v eQ u.
3. If v eQ. u and u -Q u', then v CQ u'.

A combined substitution is a pair consisting of a modal substitution and a first-order substitution. A combined substitution (uM, O'Q) is£­ admissible provided

1. u M respects £-accessibility relations, as before.
2. (K-logics only) u -M u' implies 11 eM u (and hence v eM u') for some position v.
3. <l = (< U eMU eQ)+ is irreflexive, where eM and eQ are the relations induced by O'M and O'Q respectively as described above and in § 2.5.1.

For constant-domains the appropriate notion of complementarity is as follows (for an indexed formula X") : Let u be an £-admissible com­ bined substitution for X". A connection { u, v} is u-complementary iff

For varying domains complementarity is defined in the following way: (for an indexed formula X") if u is an £-admissible combined substitution for X~', a connection { u, v} in X" is u-complementary iff

Note the addition of the third clause by which the modal and first­ order substitution interact.

Remark. We have blurred the distinction between an individual variable and the position that represents it in order to state the second condition. ·

Consequently we have:

Theorem 2.5.4 A (fir·t-order) modal formula A i· .C-valid iff there i· a multiplicityp, an .C-admi··ible combined substitution u and a ·et of u-complementary connection· that ·pan· the indexed formula (A, O)".

Once again we utilise tableau techniques to prove this theorem.

a Proof search in the matrix systems.

The matrix systems presented above reduce the task of checking a modal formula for validity to one of path checking and complemen­ tarity tests. The path checking is performed by adding connections to a set and eliminating all those atomic paths that contain the new connection. H all atomic paths can be eliminated in this manner, the formula is valid. Complementarity teats are performed aa each connec· tion is added. Bibel [Bib82b,Bib82a]ahowa how some of the atandard resolution search strategies can be utilised for this process. Hie reaulta carry over to our modalayatema without change.

Consider the example {indexed) formula of Figure 2. Ignoring the first-order features for the moment, the connection { a~ 1 ), a~~ } givea rise to the problem of unifying the prefixes ( a0a2a3a~ 1 )) and ( ao~~), where we have overlined the v0-type ("variable") positions. We can immediately see that such a connection cannot be made {proposition· ally) complementary (condition 1) unleu the acceuibility relation of the logic ia transitive. H this is the case, the {moat general) unifier sends ~~ to the sequence 42a3a~ 1 ).

The second connection { a~ 1 ), a~~ } gives rise to the problem of unifying ( aoa2a3~s 1 )) and ( aoll\~). Since 11\~ haa the value 42asa~ 1 ) under the current modal substitution, we can make the two connections (propoaitionally) complementary if we send ~ 1 ) to a~ 1 ) .

Consider now the first-order features of our example formula. In addition to the modal substitution we must build a first-order substi­ tution which unifies the labels of the connections.

For the first connection we must unify Pz( 1 ) with Py( 1 ) . This gives rise to the problem of unifying ~ 1 ) with a~~. The moat general unifier simply mapa the former position to the latter. So far so good. Consider now the second connection. That gives rise to the problem of unifying Qz( 1 ) with Qz( 1 ) 1 i.e., ~ 1 ) with a~~. Clearly we cannot build a consistent mapping for ~ 1 ) which unifies both labels.

Due to the multiplicity of a4 there ia an alternative connection { a~ 2 ) 1 a~~ } which together with the first also forma a spanning set (§ 2.4). Propoaitionally, this connection gives ua the problem of unify­ ing ( a0a2a3~ 2 )) and ( aoai~) which is easily accompliahed by map­ ping ~ 2 ) to a~ 1 ) {recall that a~~ is already mapped to 42�sa~ 11 ). At the first-order level we must unify Qz( 2 ) and Qz( 1 l, i.e., ~ 2 ) with a~~ which can now be accompliahed.

The reduction ordering induced by these substitutions ia shown aa a graph in Figure 3. Notice that it is cyclic. It is eaay to show that no increase in multiplicity can overcome this. Consequently we conclude that the formula is not valid in the first-order constant domain versions of the transitive logica.

We can alao check the third condition to determine the status of the formula with respect to the varying-domain logica. Our first-order substitution mapped ~ 1 ) to a~~ and oi 2 l to a~~. The prefix of ~ 1 ) is {aoa2a3) while the prefix of a~~ is ( a0~~ )' Under the modal substitution this latter prefix becomes ( a0a2a3a~ 1 )). Since these two prefixes cannot be unified the connections are not complementary in the varying-domain logics. {Notice that we do not even get aa far aa a cyclicity check in this caee.) The prefixes and unifien are summarised in Table 5.

The path checking procese may be interpreted aa constructing proof treea in a prefixed tableau/sequent baaed proof eyatem where the pre­ fixes contain "Skolem" variable· and are interpreted a8 "Skolem" func­ tions. The appropriate ayateme are eimilar in spirit to those of Jackson and Reichgelt [JR87]. This haa been utilised in implementations to provide a human oriented interface to the search [WW87]. Note that we are concerned with an interface to the search itself rather than the presentation of an already constructed proof for which the techniques of [And80,Mil84] are applicable.

4 Related work

There are two main approaches for extending resolution techniques to modal logica. The lirat is to reatrict the eyntactic form of formulae, so that an appropriate modal' clausal-form may be defined, and ap­ ply clausal resolution techniques (cg., [Far83]) . Bibel's comprehensive comparison of clausal resolution-baaed methods and his matrix method for lint-order logic [Bib82b] auffi.cu to demonstrate the advantages of proof search baaed on the matrix approach for modallogica presented above.

The second approach ia to reetrict the application of the resolu­ tion rule to modal contexte in which it is sound. In semantic terms this means utilising resolution within each pouible world. Inference across pouible worlds is performed by another mechanism. A badi and Manna's ayateme [AM86a,AM86b], baaed on non-clausal resolu­ tion [MW80,Mur82], form perhape the moat comprehensive extension of resolution techniques to modal logics along thue linea. The mech­ anism they employ to manage modalitiea are Hilbert-style deduction rules which are used to conjoin new formulae. For example, the modal deduction rules for S5 are:

While hand proof· ueing theee eyateme can be short, the search spaces they generate are quite redundant due to the coftftectit~e-baaed rules for manipulating modalities. Combinations of MS and M4 must be aplied to facilitate the application of M1 and M2. Only when com­ plementary aubformulae are moved into the same modal context in this manner can the resolution rule be applied. Moreover, since the ayateme are generative, rules remain applicable to old formulae throughout the proof. This should be compared with our COftftection-baaed approach and the cGlctdatio"' ueed to eetabliah validity illuetrated in the previ­ ous section. In the example there, the propositional structure of the formula defined the epace to be searched {four pouible connections) . The modal operator. were dealt with using a unification algorithm.

Konolige's eyoteme [Kon86] are baaed on tableau eystema (one tableau for each pouible world) . Ordinary resolution is utilised within each tableau and a venion of Stickel's Theory-resolution [Sti85a] used 'to manipulate modalities by creating new tableaux. Search ia compli­ cated by the need to choon auitable eete of formulae to form these new tableaux. The uee of theory resolution ia not efl'ective, in the sense that an arbitrary amount of eearch muet be performed to determine that the generation of a given resolvent is indeed eound. Konolige proposes the uee of multiple refutation procedure· to overcome theee probleme.

• [AM86aj M. Abadi and Z. Manna. Modal theorem proving. In J .H. Siekmann, editor, 8th International Conference on Auto­ mated Deduction, pagea 172-189, July 1986. Lecture Notea in Computer Science, Volume 230, Springer Verlag.
• [AM86bj M. Abadi and Z. Manna. A timely resolution. In Proceeding· of Sympo1ium on Logic in Computer Science, pages 176-186, June 1986.
• [And80j P.B. Andrews. Transforming matinga into natural deduc­ tion proofs. In W. Bibel and R. Kowalak~ editors, 5th In­ ternational Conference on Automated Deduction, pages 281292, 1980. Lecture Notea in Computer Science, Volume 87, Springer Verlag.
• [And81j P.B. Andrews. Theorem-proving via general matinga. Jour­ nal of the Auociation for Computing Machinerv, 28(2):193214, April1981.
• [Bib81j W. Bibel. On matrices with connections. Journal of the AI· &ociation for Computing Machinery, 28(4):633~45, October 1981.
• [Bib82aj W. BibeL Automated Theorem Proving. Friedr. Vieweg & Sohn, Braunschweig, 1982.
• [Bib82bj W. Bibel. A comparative atudy of several proof procedures. Artificial Intelligence, 18:269-293, 1982.
• [Bib82cj W. BibeL Computationally improved veraiona ofHerbrand'a Theorem. In J. Stern, editor, Proceeding· of the Herbrand Sympo1ium, Logic Colloquium '81, pages 11-28, North­ Holland Publiahing Co., 1982.
• [BM72j R.S. Boyer and J.S. Moore. The sharing of structure in theorem-proving programs. In B. Meltser and D. Michie, editors, Machine Intelligence 7, pages 101-116, Edinburgh University Preas, 1972.
• jFar83j L. Fariii.u-del-Cerro. Temporal reasoning and termination of programs. In S. Amarel, editor, 8th International Joint Conference on Artificial Intelligence, pagea 926-929, 1983.
• [Fit72j M.C. Fitting. Tableau method. of proof for modallogica. Notre Dame Journal of Formal Logic, Xlll:237-247, 1972.
• [Fit83j M.<;:. Fitting. Proof method. for modal and intuitioniltic logic·. Volume 169 of Synthe~e library, D. Reidel, Dordrecht, Holland, 1983.
• [HM84j J.Y. Halpern andY. Moeea. Knowledge and common knowl­ edge in a distributed environment. In Srd ACM Conference on the Principle~ of Diltributed Computing, pages 5~1, 1984.
• [HM85j J.Y. Halpern andY. Moees. A guide to the modal logics of knowledge and belief:preliminary draft. In 9th International Joint Conference on Artificial Intelligence, pagea 479-490, 1985.
• [JR87j P. Jackson and H. Reichgelt. A general proof method for lint-order modal logic. Submitted to IJCAI-87, 1987.
• [Kan57j S. Kanger. Pro11ability in logic. Volume 1 of Stockholm Stud­ ie~ in Philo1ophy, Almqvist and Wikaell, Stockholm, 1957.
• [Kon84j K. Konolige. A Ded·ction Model of Belief and ite Logic1. PhD thesis, Stanford University, 1984.
• [Kon86] K. Konolige. Resolution and quantified epiatemic logics. In · J.H. Siekmanil, editor, 8th International Conference on Au­ tomated Deduction, pages 199-208, July 1986. Lecture Notea in Computer Science, Volume 230, Springer Verlag.
• [Mil84] D.A. Miller. Expansion tree proofs and their conversion to natural deduction proofs. In R.E. Shostak, editor, 7th In­ ternational Conference on Automated Deduction, pages 375393, May 1984. Lecture Notes in Computer Science, Volume 170, Springer Verlag.
• [Moo80] R.C. Moore. Re111oning about knowledge and action. Tech­ nical Note 191, SRI International, Menlo Park, Ca., 1980.
• [Mur82] N.V. Murray. Completely non-clausal theorem proving. Ar­ tificial Intelligence, 18:67-85, 1982.
• [MW80j Z. Manna and R. Waldinger. A deductive approach to pro­ gram aynthesia. ACM Tran1action1 on Programming Lan­ guage~ and Sy&tem&, 2(1):90-121, 1980.
• [Nia83] H. Nishimura. Hauptsatl for higher-order modal logic. Jour­ nal of Svmbolic Logic, 48(3) :744-751, September 1983.
• [Pne77] A. Pneuli. The temporal logic of programs. In 18th Annual Sympo1ium on Foundation& of Computer Science, pages 4657, 1977.
• [Pra60] D. Prawits. An improved proof procedure. Theoria, 26:102139, 1960.
• [Sie84j J.H. Siekmann. Universal unification. In Shostak R.E., edi­ tor, 7th International Conference on Automated Deduction, pages 1-42, May 1984. Lecture Notes in Computer Science, Volume 170, Springer Verlag.
• [Smu68] R.M. Smullyan. Firat-Order Logic. Volume 43 of Ergebniue der Mathematik, Springer-Verlag, Berlin, 1968.
• [Smu70] R.M. Smullyan. Abstract quantification theory. In J. My­ hill and R.E. Vesley, editors, Intuitionilm and Proof Theory, pages 79-91, North Holland, Amsterdam, 1970.
• [Sti85a] M.E. StickeL Automated deduction by theory resolution. Journal of Automated Reaaoning, 1:333-355, 1985.
• [Sti85bj C. Stirling. Modal logic· for communicating ayatem1. Tech­ nical Report CSR-193-85, Dept. of Computer Science, Edin­ burgh University, 1985.
• [Wal86] L.A. Wallen. Generating connection calculi from tableau­ and sequent-baaed proof systems. In A.G. Cohn and J.R. Thomas, editors, Artificial Intelligence and it1 Application·, pagea 35-50, John Wiley & Sons Ltd., 1986.
• [WW87] L.A. Wallen and G. V. Wilson. A computationally efficient proof ayatem for S5 modal logic. In Proceeding· of AISB-87, Wiley & Sons, 1987.