Vladimir V. Rybakov

Best Unifiers in Transitive Modal Logics

Dedicated to the outstanding logician Ryszard W´ ojcicki on the occasion of his 80th birthday

Abstract. This paper offers a brief analysis of the unification problem in modal transitive logics related to the logic S4: S4 itself, K4, Grz and G¨ odel-L¨ ob provability logic GL. As a result, new, but not the first, algorithms for the construction of ‘best’ unifiers in these logics are being proposed. The proposed algorithms are based on our earlier approach to solve in an algorithmic way the admissibility problem of inference rules for S4 and Grz. The first algorithms for the construction of ‘best’ unifiers in the above mentioned logics have been given by S. Ghilardi in [16]. Both the algorithms in [16] and ours are not much computationally efficient. They have, however, an obvious significant theoretical value a portion of which seems to be the fact that they stem from two different methodological approaches. Keywords: Modal logics, unification, best unifiers, admissible rules.

1.

Introduction

There are two views on the origin of the term ‘unification’, though under precise specification both views are very close to each other. Logical unification is the problem to solve whether, for two given formulas, there is a substitution, which makes these two formulas equivalent with respect to a given logic L, and whether it is possible to describe all such substitutions. Unification in computer science is the problem of making two given terms semantically equal. This amounts to checking whether there is a substitution for two given terms, which makes them semantically equal. By this we mean a situation such that the values of these two resulting terms are the same in all models for all interpretations of variables of these terms. Initially unification in computer science started as the task of determining whether two given terms could be syntactically equal, by replacing their variables by terms. When possible, they were said to be unifiable. This notion was

Special issue in honor of Ryszard W´ ojcicki on the occasion of his 80th birthday Edited by J. Czelakowski, W. Dziobiak, and J. Malinowski Received March 17, 2011; Accepted July 15, 2011

Studia Logica (2011) 99: 321–336 DOI: 10.1007/s11225-011-9354-y

© Springer 2011

322

V. Rybakov

independently introduced in automated deduction by Robinson [29] and in term rewriting by Knuth and Bendix [25]. Then the idea transformed and instead of making terms syntactically equal, the task was to determine whether it is possible to make terms equivalent modulo a given equational theory E. This kind of unification is called (cf. Baader and Ghilardi [8]) E-unification or equational unification. Since, in most cases, non-classical logics from areas of AI and CS are duals of equational theories of special algebraic systems (such as modal, pseudo-boolean, temporal, etc. algebras) the problem of terms unification directly coincides with its logical-unification counterpart. The decision problem (namely, the question whether a given E-unification problem has an Eunifier or not) may be non-trivial for special equational theories. However, if the unification problem is decidable (for given E-theories), then one can consider its complexity (cf. [1, 5]). In case the unification problem is decidable, the question how to compute all possible E-unifiers appears (e.g. in E-unification for automated deduction and term rewriting). A natural question is how to compute a minimal complete set of Eunifiers, that is a set of E-unifiers of the given problem such that (i) every E-unifier of the problem is an instance of a unifier in this set (completeness) and (ii) two different unifiers in the set are incomparable modulo instantiation (minimality). To classify equational theories from the viewpoint of the unification problem, the unification type of equational theories has been considered. A theory E is said to be unitary (finitary, infinitary) if the cardinality of a minimal complete set of E-unifiers is at most 1 (always finite, sometimes infinite). For example, for some modal logics [12] and description logics [6] finitary unification is possible. Although there are natural examples of E-theories without finitary unification. From the viewpoint of applications, logical unification is being, in particular, a base for logic programming (for example, it is such in Prolog). This has been a focus of interest for the logical community and computer scientists for some time (cf. Baader and Nipkow [2], Baader and Snyder [5], Baader et al [3, 4, 7], Ghilardi [14, 15, 16, 17], Gabbay and Reyle [13], Oliart and Snyder [28], Levi and Villaret [27]). The unification problem (whether a formula can be unified in a given logic) is, in fact, a particular case of a more complicated problem: the substitution problem. That is, the problem whether a formula can be made a theorem after replacing some of the variables by formulas and keeping the remaing variables unchanged. This problem was studied and solved in Rybakov [31, 32, 34]) for intuitionistic logic and modal logics S4 and Grz (but only to the extent of determining if a solution exits, and computing a particular one when this was the case).

Best Unifiers in Transitive Modal Logics

323

Ghilardi [14, 15, 16, 17] studied extensively unification in propositional modal logics over K4 (using projective algebras and applying a technique of special projective formulas) with the aim of describing all possible unifiers. In these works the problem of the construction of the ‘best’ unifiers, in the logics under consideration, was solved and algorithms for the computation of ‘best’ unifiers were constructed. This approach also proved to be very useful in dealing with admissibility and bases of admissible rules [18]. In fact, when a computable finite sets of ‘best’ unifiers is constructed, a solution of admissibility problem follows immediately. Thus Ghilardi’s approach to unification gave new solutions to the problem of admissibility of inference rules for the modal logics S4, Grz, and the intuitionistic logic. And, his approach solved the same problem for K4 and GL. The admissibility problem (to determine for any given rule if this rule is admissible for a given logic) is closely related to the unification in many ways. Actually this problem grew from general research on possible ways to model human (mathematical) reasoning and to understand the essence of mathematical truth (cf. W´ ojcicki [38, 39]), in particular, from attempts to construct axiomatic derivation systems. Here the question is: which inference rules are admissible and how to identify them? This problem has been the focus of interest for many logicians (cf. Rybakov [31, 32, 35, 37, 36], Rybakov et al [9, 10], Iemhoff [19, 20], Iemhoff and Metcalfe [21], Jerabek [24, 22, 23]). In particular, in Rybakov [30] (1984) the admissibility problem was first solved for the modal logic S4 and for the intuitionistic logic Int. The innovative and impressive results of Ghilardi [15, 17] on unification, and, in particular, the complete description of best unifiers in modal logic S4 (cf. [16]) gave a computational ground to construct all unifiers. These techniques turned out to be very flexible, bringing effective computational tools to work with various problems. Naturally, such results begot interest in similar problems for non-classical logics with more computational background, for example the linear temporal logic LT L. Recently we found a way to describe most general unifiers in LT L (see Babenyshev and Rybakov [9]). The previous research, as outlined above, suggests that there is an interesting field: logical unification, its applications to CS, AI and pure mathematical logical problems (for example, admissibility of inference rules). As mentioned above, decidability of the problem of computing ‘best’ unifiers implies decidability of the problem of recognizing admissibility of inference rules. In this paper, we answer positively to the following natural question: do our previous algorithms for deciding admissibility of inference rules work (after necessary adaptation) for for the computation of ‘best’ unifiers (that is for solutions of unifiability problem in modal transitive logics)?

324

2.

V. Rybakov

Motivation

The motivation for this paper came from earlier research of the author concerning admissibilty of inference rules. In Rybakov [30], the solution to Friedman’s problem of finding an algorithm for solving admissibility of inference rules in intuitionistic logic Int was given (as well as for the modal logic S4). It was achieved via an effective (computable) construction of a unifier for the premisses of any given inference rule which disproves admissibility if the rule is not admissible. Later some algorithms for deciding admissibility of inference rules with meta-variables (coefficients) in these and similar logics were also found (cf. e.g. Rybakov [31, 32, 33, 34]). Deciding admissibility of inference rules with coefficients solves a more general problem – namely the problem of unification of formulas with coefficients. In algebraic terms, this amounts to finding an algorithm, which recognizes whether given equations in signature extended by constants for free generators are solvable in free algebras (of varieties of corresponding algebras, i.e modal algebras or pseudo-boolean algebras). Furthermore, this algorithm constructs a particular solution for solvable equations. Again, it works via a computable construction of a specific unifiers of formulas with meta-variables. Vice versa, any construction of ‘best’ unifiers for formulas with-metavariables solves the admissibility problem. Indeed, if a rule with premises ϕ1 , . . . ϕk and a conclusion ψ is not admissible, then there is an obstacle, that is a substitution which disproves ψ and unifiers ϕ1 , . . . ϕk . But then, a ‘best’ unifier for ϕ1 , . . . ϕk suffices. Thus, when all ‘best’ unifiers are constructed and the logic under question is decidable, the task is done. In particular, the connection between the problem of unification and admissibility is seen to be very tight. A natural question arises, whether the opposite direction works as well. That is whether the constructions for verification of admissibility in Rybakov [31, 32, 33, 34] may work for the construction of ‘best’ unifiers. This was our starting point. It turns out that the answer is: Yes. What is remarkable is the fact that the solution to the problem of unification turned out to be very short from methodological point of view, using proofs of earlier results and techniques of the author concerning admissible rules. A construction of ‘best’ unifiers immediately follows from these proofs by simply changing the base (first) step in the construction of obstacles for inadmissible rules in our inductive constructions. It is sufficient to use flat, not filtered models instead of filtered (or condensed) ones. All subsequent inductive steps to be the same as were before. In all cases, at most one page long modernization is

325

Best Unifiers in Transitive Modal Logics

necessary, and constructions of best unifiers follow immediately. Complexity of these algorithms for computation of best unifiers is not better than that of those previously known, and they have no advantage in this respect. The only theoretical advantage they may have is that they stem from different methodological approach.

3.

Definitions and Preliminary Facts

In this paper we will use standard notations, facts and definitions concerning modal propositional logics and their Kripke-Hintikka semantics. In particular, a Kripke frame is a pair (F, R), where F is a non-empty set, and R is a binary relation on this set (in our paper, R is always transitive). A Kripke model is a frame with a fixed valuation V for a set of propositional letters. Modal formulas have the standard definition for truth values at worlds (elements) of Kripke models. The notation (F, a) V ϕ means that the formula ϕ is true at the world a of F = (F, R) with respect of the valuation V . We write F ϕ, if for any valuation V , the formula ϕ is true at any world of F w.r.t. V ; in this case we say ϕ is true at the frame F. For a set of frames S, L(S) is the set of all modal formulas which are true at any frame from S. In particular, the modal logic S4 is L(RT ), where RT is the set of all reflexive and transitive frames. K4 = L(T ), where T is the set of all transitive frames. A logic L is said to have the finite model property (fmp in the sequel), if L = L({F : F is finite and F

ϕ for every ϕ ∈ L}).

In particular, K4, S4, Grz, and GL have fmp. Let F orK4 be the set of all formulas in the language of K4 and ε be a mapping (we will refer to ε as substitution) of a set of letters Dom(ε) in F orK4 . Any such mapping ε can be extended to the set of all formulas in letters from Dom(ε), by ε(ϕ(x1 , . . . , xn )) := ϕ(ε(x1 ), . . . , ε(xn )). A formula ϕ is unifiable in L if there is a substitution ε (which is called a unifier for ϕ), such that ε(ϕ) ∈ L (in the sequel, we use the notation ϕε := ε(ϕ) in those cases in which it is more readable in complex expressions). Definition 1. A unifier ε is more general than an unifier ε1 iff there is a substitution δ such that for any letter x, ε1 (x) = δ(ε(x)).

326

V. Rybakov

If a logic L is decidable, to check unifiability of a formula in L is an easy task: it is sufficient to use only ground substitutions, that is mappings of letters in the set {⊥, }. The problem is how to find (compute) all possible unifiers. In what follows, we will use special n-characterizing Kripke models with definable elements, construction of which was given in [30] for the logic S4 (for any modal transitive logics with fmp, cf., for instance, [34]). The construction is as follows. Let a modal transitive logic L with fmp be given, let n be a natural number. Sl1 (Ch(L)) is the model (with the valuation V of letters p1 , . . . , pn ), which consists of all (non-isomorphic) clusters with valuation V of letters p1 , . . . , pn , where (i) the clusters do not contain duplications (worlds with the same valuation of p1 , . . . , pn w.r.t. V ) and (ii) each such cluster, as a frame, is an L-frame. Assume the model Slk (Ch(L)), for k ∈ N , is already constructed. Let ACk be the set of all anti-chains of clusters from Slk (Ch(L)), each of which contains at least one cluster of depth k. For each X ∈ ACk , and each cluster C from Sl1 (Ch(L)), we take the copy M (C) of C (as the model) and adjoin it (disjointly) to Slk (Ch(L)), and assume worlds from Slk (Ch(L)) to be accessible from worlds of M (C) iff they are accessible from some worlds of X. Then, we delete all clusters M (C) which would not generate an L-frame, and those M (C) which are adjoined using anti-chains consisting of only one cluster C, where M (C) is a submodel of C. We set 

Ch(L)n :=

Slk (Ch(L)).

k∈N

By fmp of L, it is straightforward to verify that (i) Ch(L)n is an n-characterizing for L (that is, for any formula ϕ in letters p1 , . . . , pn , ϕ ∈ L ⇔ Ch(L)n ϕ) and (ii) any world of Ch(L)n is definable, that is, for any world w of Ch(L)n , there is a formula ϕ in letters p1 , . . . , pn , such that for any world s, (Ch(L)n , s) V ϕ ⇔ s = w. (for proof if desired, see p. 434 [34]). We will need transformation of formulas in their reduced normal forms (cf. [30], or [34]). A formula ϕ is said to be in reduced normal form if ϕ=



(



t(j,i,0)

[xi

∧ (3xi )t(j,i,1) ]),

1≤j≤m 1≤i≤n

where xs are some variables (letters), and t(j, i, z), t(j, i, k, 0) ∈ {0, 1} and, for any formula α above, α0 := α, α1 := ¬α. For any formula ϕ, V ar(ϕ) denotes the set of all letters (variables) from ϕ.

Best Unifiers in Transitive Modal Logics

327

Definition 2. Let ϕrf be a formula in reduced normal form. ϕrf is said to be a reduced normal form for a formula ϕ iff (a) V ar(ϕ) ⊆ V ar(ϕrf ); (b) For any frame F and for any world a from F and any valuation V in F, if (F, a) V ϕ then there is an extension V1 of V to additional variables of ϕrf , such that (F, a) V1 ϕrf ; (c) For any frame F and any valuation V1 of letters from ϕrf , if, for any world a from F, (F, a) V1 ϕrf , then for any world b, (F, b) V ϕ, where V is restriction of V1 to variables of ϕ. In [30], we proved the following theorem. Theorem 3. There exists an algorithm running in (single) exponential time, which, for any given formula ϕ, constructs its reduced normal form ϕrf . Proof. Assume ϕ is given. For any letter p of ϕ, we pick xp := p. If ψ is a proper (that is not a letter) subformula of ϕ, let xψ be a new letter. If ψ = α ◦ β, where ◦ is a binary operation, the extension formula for ψ is xψ ≡ xα ◦ xβ . If ψ = β, where  is a unary operation, the extension formula for ψ is xψ ≡ xβ . Let ϕ1 be conjunction of xϕ and all the extension formulas. It is clear that (a) – (c) from Definition 2 hold for ϕ and ϕ1 , and the size of ϕ1 is linear in ϕ. Next, we transform ϕ1 to the perfect disjunctive normal form (which then has the disjunctive members of uniform form and length, each of which contains all the components required in the definition of unfolded formulas) and obtain as the result the formula ϕ2 . This transformation, as well as all known ones for reduction of Boolean formulas to disjunctive normal forms, is exponential. Thus ϕ2 is a reduced normal form for ϕ. The reduced normal form for ϕ constructed by the algorithm given in this theorem is unique. Lemma 4. The following holds for any logic L = L(SF ) (for some SF ), (i) ϕ is unifiable in L iff ϕrf is unifiable in L. (ii) if ε is a unifier for ϕ in L, then an extension of ε to additional variables of ϕrf is a unifier for ϕuf . (iii) if ε is a unifier for ϕrf , then the restriction of this unifier to only letters of ϕ is a unifier for ϕ. Proof. Immediately follows from the choice of ϕ1 in Theorem 3.

328

V. Rybakov

We need to recall the construction of special Kripke models  by reduced normal forms of formulas. Let ϕ be a formula and ψ := j∈J ϕj be its reduced normal form as constructed in Theorem 3.  A model M(ψ) is a model having as its base set a set of formulas ϕj from j∈J ϕj (in the sequel, in case of applications, these sets will be specified). The valuation V of all letters from ψ is defined as follows: V (xi ) is the set of all ϕj from the base set, where xi , as letters not bounded by 3, occur only positively. To define the accessibility relation R in this model we need the following notations. For any ϕj , θ1 (ϕj ) is the set of all letters, which, as letters not bounded by 3, occur only positively in ϕj . For any ϕj , θ2 (ϕj ) is the set of all letters xi , such that 3xi occurs positively in ϕj . The accessibility relation R for any such model is given by ϕj Rϕl ⇔ θ2 (ϕl ) ⊆ θ2 (ϕj ). A set of unifiers SU of a formula ϕ in a logic L is a set of best unifiers for ϕ in L, if the following holds: for any unifier σ for ϕ in L, σ is a substitutional example of some unifier σb (that is σb is more general than σ) from SU .

4.

Best Unifiers for S4

In the light of Lemma  4, we may consider only formulas in reduced normal form. If ϕ := j∈J ϕj is a formula in reduced normal form and ϕ is unifiable in S4 by a unifier σ, then, as shown in Rybakov [30] (or, as it was later stated in Lemma 3.9.4 from [34]) there is  a model M(ϕ) on some disjuncts ϕj as worlds described above, such that ϕj ∈M(ϕ) ϕσj ∈ S4, and the following holds: (i) θ1 (ϕj ) ⊆ θ2 (ϕj ) for any ϕj from M(ϕ); (ii) for all ϕj ∈ |M(ϕ)|, ϕj

V ϕj ;

(iii) for exists ϕX ,j ∈ |M(ϕ)| such that  any X ⊆ |M(ϕ)|, there  θ2 (ϕX ,j ) = θ1 (ϕX ,j ) ∪ ϕj ∈X θ2 (ϕj ) .  Let, for any ϕ = j∈J ϕj , SM (ϕ, S4) be the set of all models on disjuncts ϕj described above, satisfying conditions (i), (ii), and (iii) (if ϕ is unifiable, as it is mentioned above, such models exist). For any M ∈ SM (ϕ, S4), and ϕj ∈ M take the formulas   γj := ϕj ∧ (2 ϕk ) and γ(M) := γj . ϕj Rϕk ,ϕk ∈M(ϕ)

ϕj ∈M(ϕ)

329

Best Unifiers in Transitive Modal Logics

Take the model Ch(S4)k (where k is the number of letters in ϕ) with its own valuation V and the generated submodel V (γ(M)) of Ch(S4)k (that is — all worlds from Ch(S4)k , where γ(M) is true w.r.t. the valuation V ). Then the formula ϕ is true in V (γ(M)) w.r.t. the valuation V . If we take the following definable valuation S for letters from the formula ϕ, 

S(xi ) := γ(M) ∧ [

ϕj ],

xi ∈θ1 (ϕj ),ϕj ∈M(ϕ)

S will coincide with the valuation V on V (γ(M)) and, in particular, ϕ is valid in V (γ(M)) w.r.t. the valuation S. Now we apply (verbatim) the reasoning from Rybakov [30] (or the proof of Lemma 3.4.10, starting at page 318, from [34]) and extend S from V (γ(M)) to a definable valuation SM on the entire model Ch(S4)k , where ϕ is true w.r.t. SM at all the worlds from Ch(S4)k . Properties (i), (ii) and (iii) (as given above) are necessary for this. This new valuation SM is effectively constructed (in [30], or in [34]), and an algorithm for writing out formulas defining the valuation SM is given there. As the result, we get that ϕ is true in Ch(S4)k w.r.t. SM , so, SM gives us a unifier for ϕ in S4, and the valuation SM coincides on V (γ(M)) with S (this is because the extension of S to SM keeps the values at V (γ(M)) intact). Thus, the following holds: Lemma 5. For any M ∈ SF (ϕ, S4), the substitution σM defining SM is a unifier for ϕ and the valuation SM coincides on V (γ(M)) with S. Lemma 6. For any unifier σ for ϕ, there are M ∈ SM (ϕ, S4) and a substitution β, such that σ(xi ) ≡S4 β(σM (xi )). Proof. We show that σ(xi ) ≡S4 σ(σM (xi )). Indeed, take Ch(S4)k , where k is the number of all letters occurring in all σ(xi ) and take an a ∈ Ch(S4)k . Since σ is a unifier for ϕ, as we have seen above, there is a corresponding model M(σ) ∈ SM (ϕ) consisting of some disjuncts ϕj with the mentioned properties (i) – (iii), and, in particular, Ch(S4)k

 V

ϕσj .

ϕj ∈M(ϕ)

Then, in particular, Ch(S4)k

 V ϕj ∈M(σ)

γjσ and Ch(S4)k

Vγ

σ

(M).

330

V. Rybakov

Thus, V (γ σ (M)) = Ch(S4)k . Besides, by Lemma 5, Ch(S4)k V σ(γ(M)) → [σ(xi ) ≡ σM (σ(xi ))]. In particular, for any letter xi , a

V σ(xi )

⇔a

V σM (σ(xi )).

Thus, all constructed unifiers σM defining substitutions SM (cf. Lemma 5) gives us the finite set of best unifiers for ϕ in S4. Computational complexity of our construction for these unifiers is not better than those obtained earlier in S. Ghilardi [16]. The interesting point here is that we write out formulas for best unifiers directly and explicitly by an inductive procedure.

5.

Best Unifiers for K4, Grz, and GL

Here we will modify results from the previous section to transitive modal logics from the S4 area — K4, Grz, GL – in order to give algorithms for the construction of best unifiers in these logics. Recall that K4 := L({F | F Grz := L({F | F GL := L({F | F

is a finite transitive frame }); is a finite partialy ordered set});

is a finite transitive and ireflexive frame }).

In particular, all these logics have fmp. Recall that a frame F is irreflexive if, for any world a from F, aRa does not hold. In order to find a construction of best unifiers in these logics it is sufficient to use the technique from the previous section and to modify, a bit, the previous technique of the author (cf. for example, [34]) to find obstacles for inadmissible inference rules. Case: K4. If we work with the logic K4, modernization of our procedure starts from construction of the models M(ϕ) generated by formulas ϕ in a normal reduced form. In this case, any such model M(ϕ) again has as the base set some set of formulas ϕj . The valuation V of letters from ϕ is defined as before. Sets θ1 (ϕj ) and θ2 (ϕj ) are as earlier. However, the accessibility relation is modified: ϕj Rϕl ⇔ [θ2 (ϕl ) ∪ (θ1 (ϕl )] ⊆ θ2 (ϕj ).

331

Best Unifiers in Transitive Modal Logics

If ϕ is a formula in reduced normal form unifiable in K4 then, as it is shown in Lemma 3.9.1 from [34], there is a model M(ϕ) with some disjuncts ϕj as worlds, described above, such that, ϕj ∈M(ϕ) ϕσj ∈ K4 and (1.1) For all ϕj ∈ |M(ϕ)|, ϕj

V ϕj .

For any X ⊆ |M(ϕ)|, (2.1) ∃ϕX ,j,1 ∈ |M(ϕ)| [θ2 (ϕX ,j,1 ) = θ1 (ϕX ,j,1 ) ∪



(θ2 (ϕj ) ∪ θ1 (ϕj ))];

ϕj ∈X

(2.2) ∃ϕX ,j,2 ∈ |M(ϕ)| [θ2 (ϕX ,j,2 ) =  

(θ2 (ϕj ) ∪ θ1 (ϕj ))].

ϕj ∈X

For any ϕ = j∈J ϕj , in a normal reduced form, SM (ϕ, K4) is the set of all models on disjuncts ϕj described above, satisfying conditions (1.1), (2.1), and (2.2) (if there are any such models). We consider any M ∈ SM (ϕ) and construct the formula γ(M) and the valuation S for ϕ as in the previous section (but we refer now to K4 rather than S4). Thereafter we again, as in the previous section, extend S to the whole model Ch(K4)k , and get a definable valuation SM , where ϕ is true w.r.t. SM in the whole model Ch(K4)k . In this case, we use reasoning from Lemma 3.4.10 (page 384) from [34] and properties (1.1), (2.1) and (2.2). The formulas defining SM will then be effectively written out. Again, SM will coincide with S on V (γ(M). As a consequence we get Lemma 7. For any M ∈ SF (ϕ, K4), the substitution σM defining SM(σ) is a unifier for ϕ in K4 and the valuation SM(σ) coincides on V (γ(M)) with the valuation S. Lemma 8. For any unifier σ for ϕ in K4, there are M ∈ SM (ϕ, K4) and a substitution β, such that σ(xi ) ≡K4 β(σM (xi )). The proof follows verbatim that of Lemma 6. By these two lemmas, all constructed σM give us a set of best unifiers for ϕ in K4. Case: Grz.

332

V. Rybakov

For this case, we again change the definition of the models M(ϕ) constructed from formulas ϕ in a normal reduced form. The valuation V of all letters from ϕ is defined as before, and with the sets θ1 (ϕj ) and θ2 (ϕj ) defined as in the previous section. The definition of the accessibility relation is new. The model M(ϕ) has some special accessibility relation which is a partial order ≤ defined as follows: θ2 (ϕl ) ⊂ θ2 (ϕj ) ⇒ ϕj ≤ ϕl , and, for any set of formulas ϕj with the same θ2 (ϕj ), this set is just ordered by ≤ as a linear order. If ϕ is a formula in reduced normal form, which is unifiable in Grz then, as it is shown in [31] (or in Lemma 3.9.7 from [34]), there is a model M(ϕ) with some disjuncts ϕj as worlds, as described above, such that  σ ϕj ∈M(ϕ) ϕj ∈ Grz and (3.1) θ1 (ϕj ) ⊆ θ2 (ϕj ) for any ϕj from M(ϕ); (3.2) For all ϕj ∈ |M(ϕ)|, ϕj

V ϕj ;

(3.3) ∀X ⊆ |M(ϕ)|, there is a ϕX ,j ∈ |M(ϕ)|  such that  θ2 (ϕX ,j ) = θ1 (ϕX ,j ) ∪ ϕj ∈X (θ2 (ϕj ) . So, these models are similar to those in the case of S4, but are partially  ordered. For any ϕ = j∈J ϕj in reduced normal form, SM (ϕ, Grz) is the set of all models on disjuncts ϕj described above, satisfying conditions (3.1), (3.1) and (3.2) (if there are any such models). We consider any M ∈ SM (ϕ, Grz) and construct the formula γ(M) and the valuation S for letters of ϕ as in the previous section (only we now refer to Grz rather than S4). Now, we extend S to the whole model Ch(Grz)k , and get a definable valuation SM such that ϕ is true w.r.t. SM in the whole model Ch(Grz)k . In this case, we use reasoning from [31] (or from Lemma 3.4.10 from [34]). It is sufficient merely to check the details through these constructions. Properties (3.1), (3.2) and (3.3) above to be essentially used. In the process, the formulas defining SM will be effectively written out. Again, SM will coincide with S on V (γ(M). Consequently we obtain Lemma 9. For any M ∈ SF (ϕ, Grz), the substitution σM defining SM(σ) is a unifier for ϕ in Grz and the valuation SM(σ) coincides on V (γ(M)) with the substitution S. Lemma 10. For any unifier σ for ϕ in Grz, there are M ∈ SM (ϕ, Grz) and a substitution β, such that σ(xi ) ≡K4 β(σM (xi )).

Best Unifiers in Transitive Modal Logics

333

The proof follows verbatim that of Lemma 6. Q.E.D. By these two lemmas, all constructed σM give us a finite, effectively computable set of best unifiers for ϕ in Grz. Case: GL. We need to modify the definition of the models M(ϕ) constructed from formulas ϕ in reduced normal form. The valuation V of all letters from ϕ is defined as before, and also the sets θ1 (ϕj ) and θ2 (ϕj ) are defined as in the previous section. The definition of the accessibility relation is new, it should be now an irreflexive relation. We set: ϕj < ϕl ⇔ [θ2 (ϕl ) ⊂ θ2 (ϕj ) & θ1 (ϕl ) ⊆ θ1 (ϕj )]. If ϕ is a formula in reduced normal form which is unifiable in GL, then as shown in [33] (or in Lemma 3.9.10 from [34]), there is a model M(ϕ) with some set of disjuncts ϕj as worlds, as described above, such that  σ ϕj ∈M(ϕ) ϕj ∈ GL and (4.1) For all ϕj ∈ |M(ϕ)|, ϕj

V ϕj ;

(4.2) ∀X ⊆ |M(ϕ)|, there is an ϕX ,j ∈ |M(ϕ)|, such that   θ2 (ϕX ,j ) = ϕj ∈X (θ2 (ϕj ) ∪ θ1 (ϕj )) .  Next, for any ϕ = j∈J ϕj in a reduced normal form, SM (ϕ, GL) is the set of all models on disjuncts ϕj described above, satisfying conditions (4.1) and (4.2) (if there are any such models). We consider any M ∈ SM (ϕ, GL) and construct the formula γ(M) and the valuation S for letters of ϕ as in previous section (only now referring to GL rather than S4). Now, similar to previous section, we extend S to the whole model Ch(GL)k , and get a definable valuation SM w.r.t. which ϕ is true in the whole model Ch(GL)k . For this case, we use reasoning from [33] (or Lemma 3.4.10 from [34]), and the properties (4.1) and (4.3). We follow in detail the procedure for the extension of the valuation S. The formulas defining SM will again be effectively written out in the process. Again, SM will coincide with S on V (γ(M). Hence we conclude Lemma 11. For any M ∈ SF (ϕ, GL), the substitution σM defining SM(σ) is a unifier for ϕ in GL and the valuation SM(σ) coincides on V (γ(M)) with the valuation S. Lemma 12. For any unifier σ for ϕ in GL, there are M ∈ SM (ϕ, GL) and a substitution β, such that σ(xi ) ≡GL β(σM (xi )).

334

V. Rybakov

The proof follows verbatim the one given for Lemma 6. Q.E.D. By these two lemmas, all constructed σM give a finite, effectively computed set of best unifiers for ϕ in GL. The technique offered here is rather flexible and we can apply it successfully, for example, to modal logic S4.1 and S4.2. Acknowledgements. Supported by Engineering and Physical Sciences Research Council (EPSRC), U.K., grant EP/F014406/1. References [1] Baader, F., and J. H. Siekmann, ‘Unification theory’. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press, Oxford, UK, 1994, pp. 41–125. [2] Baader, F., and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998. ¨sters, Unification in a Description Logic with Transitive [3] Baader, F., and R. Ku Closure of Roles. LPAR 2001, pp. 217–232. [4] Baader, F., and P. Narendran, ‘Unification of Concept Terms in Description Logics’. J. Symb. Comput. 31(3):277–305, 2001. [5] Baader, F., and W. Snyder, ‘Unification Theory’. In J. A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, volume I. Elsevier Science Publishers, 2001, pp. 447–533. [6] Baader, F., D. Calvanese, D. McGuinness, D. Nardi, and P. F. PatelSchneider (eds.), The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. [7] Baader, F., and B. Morawska, ‘Unification in the Description Logic EL’. Logical Methods in Computer Science 6(3):1–31, 2010. [8] Baader, F., and S. Ghilardy, ‘Unification in modal and description logics’. Logic J. of IGPL 2010, doi: 10.1093/jigpal/jzq008, First published online: April 29, 2010. [9] Babenyshev, S., and V. Rybakov, ‘Linear Temporal Logic LTL: Basis for Admissible Rules’, J. Logic Computation 2010, doi: 10.1093/logcom/exq020,21. [10] Babenyshev, S., and V. Rybakov, ‘Unification in Linear Temporal Logic LTL’, 2010, submitted. [11] Babenyshev, S., V. Vladimir, R. Schmidt, and D. Tishkovsky. ‘A tableau method for checking rule admissibility in S4’. In Proc. of the 6th Workshop on Methods for Modalities (M4M-6), Copenhagen, 2009. [12] Blackburn, P., J. van Benthem, and F. Wolter (eds.), The Handbook of Modal Logic. Elsevier, 2006. [13] Gabbay, D., and U. Reyle, ‘N-Prolog: - An extension of Prolog with hypothetical implications’, Journal of Logic Programming 1:391–355, 1984. [14] Ghilardi, S., ‘Unification Through Projectivity’. J. Log. Comput. 7(6):733–752, 1997.

Best Unifiers in Transitive Modal Logics

335

[15] Ghilardi, S., ‘Unification in intuitionistic logic’, J. Symb. Log. 64(2):859–880, 1999. [16] Ghilardi, S., ‘Best solving modal equations’, Ann. Pure Appl. Logic 102(3):183–198, 2000. [17] Ghilardi, S., ‘Unification, finite duality and projectivity in varieties of Heyting algebras’. Ann. Pure Appl. Logic 127(1-3):99–115, 2004. [18] Iemhoff, R., ‘On the admissible rules of intuitionistic propositional logic’. J. Symb. Log. 66(1):281–294, 2001. [19] Iemhoff, R., ‘On The Admissible Rules of Intuitionistic Propositional Logic’. J. Symb. Log. 66(1):281–294, 2001. [20] Iemhoff, R., Towards a Proof System for Admissibility. CSL 2003, pp. 255–270. [21] Iemhoff, R., and G. Metcalfe, ‘Proof theory for admissible rules’. Ann. Pure Appl. Logic 159(1–2):171–186, 2009. [22] Jerabek, E., ‘Admissible rules of modal logics’, Journal of Logic and Computation 15(4):411–431, 2005. [23] Jerabek, E., ‘Independent bases of admissible rules’, Logic Journal of the IGPL 16(3):249–267, 2008. [24] Jerabek, E., ‘Admissible rules of Lukasiewicz logic’, Journal of Logic and Computation 20(2):425–447, 2010. [25] Knuth, D. E., and P. B. Bendix, ‘Simple word problems in universal algebras’. In J. Leech (ed.), Computational Problems in Abstract Algebra. Pergamon Press, Oxford, 1970. ¨ ger, F., and S. Merz, Temporal Logic and State Systems, Texts in Theoretical [26] Kro Computer Science. An EATCS Series, Springer, Berlin Heidelberg, 2008. [27] Levy, J., and M. Villaret, Nominal Unification from a Higher-Order Perspective. RTA 2008, pp. 246–260. [28] Oliart, A., and W. Snyder, ‘Fast algorithms for uniform semi-unification’. J. Symb. Comput. 37(4):455–484, 2004. [29] Robinson, J. A., ‘A machine oriented logic based on the resolution principle. J. of the ACM 12(1):23–41, 1965. [30] Rybakov, V. V., ‘A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic’, Algebra and Logica 23(5):369–384, 1984. [31] Rybakov, V. V., ‘Problems of Substitution and Admissibility in the Modal System Grz and in Intuitionistic Propositional Calculus’. Ann. Pure Appl. Logic 50(1):71–106, 1990. [32] Rybakov, V. V., ‘Rules of Inference with Parameters for Intuitionistic Logic’. J. Symb. Log. 57(3):912–923, 1992. [33] Rybakov, V. V., ‘Logical equations and admissible rules of inference with parameters in modal provability logics’. Studia Logica 49(2):215–239, 1990. [34] Rybakov, V. V., Admissible Logical Inference Rules. Series: Studies in Logic and the Foundations of Mathematics, Vol. 136, Elsevier Sci. Publ., North-Holland, 1997. [35] Rybakov, V. V., ‘Logics with the universal modality and admissible consecutions’. Journal of Applied Non-Classical Logics 17(3):383–396, 2007. [36] Rybakov, V. V., ‘Linear temporal logic with until and next, logical consecutions’, Ann. Pure Appl. Logic 155(1):32–45, 2008.

336

V. Rybakov

[37] Rybakov, V. V., ‘Multi-modal and Temporal Logics with Universal Formula – Reduction of Admissibility to Validity and Unification’. J. Log. Comput. 18(4):509– 519, 2008. ´ jcicki, R., ‘Theories, Theoretical Models, Truth, part I; Popperian and non[38] Wo Popperian Theories in science’, Foundations of Science 1:337–406, 1995/96. ´ jcicki, R., ‘Theories, Theoretical Models, Truth, part II: Tarski’s theory of [39] Wo truth and its relevance for the theory of science’, Foundations of Science 4:471–516, 1995/96.

Vladimir V. Rybakov School of Computing, Mathematics and IT Manchester Metropolitan University Chester Street Manchester, M 1 5GD, UK and Mathematical Institute Siberian Federal University Krasnoyarsk, Russia [email protected]