How to Use Modalities and Sorts in Prolog

Andreas Nonnengart

Max-Planck-Institut für Informatik, Im Stadtwald, 66123 Saarbrücken, Germany, Tel.: (+49) 681 302 5369, Fax: (+49) 681 302 5401, Email: Andreas.Nonnengart@mpi-sb.mpg.de

Abstract. Standard logic programming languages like Prolog lack the possibility of dealing with modalities and/or sorts. A first idea how to overcome this problem (and that without changing anything on Prolog itself) would be to apply the well-known relational translation approaches from modal and sorted logic into first-order predicate logic and to feed this translation result into Prolog. This, however, leads into other problems: firstly, the transformed problem is usually of much bigger size (number of clauses) than the original one and, secondly, very often it is not even in Horn form anymore. In this paper a translation approach is proposed which avoids both of these problems, i.e. the number of clauses after translation is exactly as big as it would have been if we simply ignored the modal operators and sort restrictions and, also, the result is in Horn form provided it was already before (modulo modal operators and sorts).

1 Introduction

For many applications in the AI community (as for instance knowledge representation and taxonomic reasoning for several agents) there is a need for modalities and/or sort declarations. On the other hand, one of the most popular AI programming languages is Prolog and it is thus evident that a combination of Prolog with modalities and sorts apparently makes sense for AI implementations.

However, it is not at all obvious how modalities and sorts could be integrated into Prolog without changing Prolog itself. A first idea might be to use standard relational translation techniques into first-order predicate logic as they are perfectly well known from the literature. With these techniques it would be possible to translate modal and sorted logic programs into classical logic before being fed to the logic programming environment.

However, soon one will have to realize that there occur quite a lot of problems with this approach. First, in the extension by modalities, the translation results in an exponential explosion of the output formula. Also, certain properties of the underlying accessibility relation, as for example symmetry, result in clauses which inevitably lead to infinite loops under the Prolog control stucture. And finally, for both modal logics and sorted logics, the resulting formula is not necessarily in Horn form even if the original formula was (if we ignored the modalities or the sort declarations respectively).

The translation approach proposed in this paper avoids these difficulties. Its theoretical basis has already been introduced in [4], although the possible application to logic programming has not been mentioned there (but in [3]) and the application to sorted logic has not been published before at all.

One of the most remarkable things about this approach is that it very often allows a significant simplification of the background theory given by the modal logic accessibility relation properties and sort declarations.

Note that this method is very closely related to the functional translation approach proposed by Ohlbach in [5], [6], [7] and others. At least the idea of replacing occurrences of certain binary predicates by suitable sets of functions is in essence identical to the approach presented there. Nevertheless, there are some quite important differences between the functional translation method and the one propose here. In the functional translation, theory clauses which stem from certain properties of the underlying accessibility relation get replaced by more or less complicated equations. These require either a pretty strong equality handling of the inference procedure or a theory unification algorithm which suits to the theory induced by the equations. Usually, however, neither of these features are available in standard logic programming languages like Prolog. Therefore, if we want to avoid changes in the logic programming language itself, we have to think of something else. Indeed, the translation approach presented in this paper does not require any changes in the programming language at all. To some extent it can be viewed as a mixed approach between relational and functional translation which tries to combine advantages from both and also tries to avoid their respective disadvantages as much as possible.

This paper is organized as follows: section 2 contains the basics of the relational translation for modal and sorted logics. Section 3 then explains how the functional simulation approach works and how it can be applied to modal and sorted logics. After that a certain saturation technique is introduced which allows to considerably simplify the background theories (for modal logics). Finally, the effect of the overall approach is demonstrated with two examples.

2 Relational Translation

Here and in the sequel we assume that the reader is already familiar with the basic principles of modal and sorted logics. Also, proofs are usually omitted in this section. In case the reader is interested in these s/he is referred to [4] and [3].

The idea of the relational translation is to make the implicit semantics of the extra features of the underlying logic explicit in the translation. I.e. in case of modal logics each predicate symbol, say P, gets replaced by a new predicate symbol, say P′, which accepts one more argument, namely (a symbol denoting) the current (or actual world) (similar for function symbols). In addition, two new predicate symbols are to be introduced, R and E, which represent the accessibility relation and the domain element existence predicate respectively (in case of varying domains).

The relational translation approach for sorted logic as it is presented here is maybe not exactly as the reader might expect. For reasons which will become clear later it is not the case that for each sort symbol a unary predicate symbol is introduced. Rather a single binary predicate symbol S will be used to express elementship of domain elements in a certain sort which itself is represented by a constant.

2.1 (Serial) Modal Logics

The relational translation approach for modal logics is defined as follows:

Definition 1. The formula morphism ⌊Φ⌋_{u} which accepts a modal logic formula and a symbol denoting a world is defined as:

⌊x⌋_{u}  = x
⌊f(t_{1}, …, t_{n})⌋_{u} = f′(u, ⌊t_{1}⌋_{u}, …, ⌊t_{n}⌋_{u})
⌊P (t_{1}, …, t_{n})⌋_{u} = P′(u, ⌊t_{1}⌋_{u}, …, ⌊t_{n}⌋_{u})

The case for the usual connectives should be clear

⌊∀x Φ⌋_{u}  = ∀x E(u, x) ⇒ ⌊Φ⌋_{u}
⌊∃x Φ⌋_{u}  = ∃x E(u, x) ∧ ⌊Φ⌋_{u}
⌊□Φ⌋_{u}  = ∀v R(u, v) ⇒ ⌊Φ⌋_{v}
⌊◇Φ⌋_{u}  = ∃v R(u, v) ∧ ⌊Φ⌋_{v}

The initial call for the translation of an arbitrary formula Φ is thus ⌊Φ⌋_{ι}, where ι denotes the initial (or actual) world.

Translating a given modal logic program (and query) with the help of the formula morphism from above is evidently not enough if the accessibility relation obeys certain extra properties as e.g. reflexivity, transitivity or symmetry. These properties have to be made explicit as well. Therefore there are usually some extra clauses to be added to the clause set after translation, namely those which reflect the background theory.

Theorem 2. Relational translation is sound and complete, i.e. Φ is (modal logic) satisfiable iff ⌊Φ⌋_{ι} ∧ ML is (predicate logic) satisfiable, where ML denotes those formulae which stem from the additional properties of the accessibility relation of the modal logic under consideration.

Proof. Can be found in [3].

Thus, in principle, it is possible to translate modal logic programs and queries into predicate logic and feed the result (up to the possibility of a getting non-Horn programs) into Prolog. However, as it turns out, this is not very satisfactory. Mainly there are two problems: one is that there is an exponential explosion in the size and the number of clauses because of the translation. Another, even more restrictive effect is that usually Prolog does not terminate when it is fed with these translated versions of the original modal logic program. The following example illustrates this:

Example 1. Consider the simple program: ◇□◇P and suppose the question is whether ◇P holds (i.e. the query is: ⇐ □P). Moreover assume that the modal logic under consideration is KDB, i.e. the accessibility relation is serial and symmetric. Negation, relational translation and transformation into Horn form results in the following Horn clause set:

From ◇□◇P

R(ι, a).

R(x, b(x)) ⇐ R(a, x).
P (b(x)) ⇐ R(a, x).

Symmetry and Seriality

R(u, v) ⇐ R(v, u).

R(u, f(u)).

The query

⇐ P (y), R(ι, y).

Running this as a Prolog program results in an infinite loop. In fact, a closer examination of the clause set shows that there is no possible arrangement of the given clauses such that an infinite loop can be avoided, although the set of clauses is indeed unsatisfiable.

The method presented later avoids such infinite loops and, in addition, reduces the number (and sometimes size) of clauses after translation considerably.

2.2 Sorted Logic

Definition 3. The formula morphism ⌈Φ⌉ which accepts a sorted logic formula Φ and returns a predicate logic formula is defined as:

\begin{aligned}⌈∀x: A Φ⌉ & = & ∀x S(a, x) ⇒ ⌈Φ⌉ \\ ⌈∃x: A Φ⌉ & = & ∃x S(a, x) ∧ ⌈Φ⌉ \\ ⌈A ⊑ B⌉ & = & ∀x S(a, x) ⇒ S(b, x) \\ ⌈e: A⌉ & = & S(a, e) \end{aligned}

where A, B are arbirary sorts and Φ is an arbitrary (sorted logic) formula. For the other logical connectives just apply the usual homomorphic extension of the above.

Note that, instead of introducing unary predicate symbols for the sorts, we just add a single new (binary) predicate symbol, namely S, and for each sort a new constant such that S(a, x) simply means that x belongs to the sort A. This has no effect on the soundness and completeness of the translation; it just fits better to the way we handled modalities.

Theorem 4. Relational translation for sorted logics is sound and complete, i.e. for any sorted logic formula Φ: Φ is (sorted logic) satisfiable iff ⌈Φ⌉ is (predicate logic) satisfiable.

Here again we have the difficulty that the translation of some sorted Horn formula is not necessarily Horn after translation (as an example consider the formula ∃x: A P (x)∨∃y: B ¬Q(y)). In the following section we will describe how this problem can be solved.

3 Functional Simulation of Binary Relations

3.1 Basic Principles

The last section provides a possibility of translating modal logic or sorted logic programs (formulae) into predicate logic by introducing new auxiliary predicates, namely R (which represents the accessibility relation for modal logics), E (which denotes the existence relation for domain elements in worlds), and S (for the “iselement-of-sort” relation for sorted logics). These are called auxiliary predicates since they do not occur in the original formulae; they are introduced by the translation. What is interesting about these predicates is that they occur solely in particular places inside formulae, namely either as ∀x P (α, x) ⇒ … or as ∃x P (α, x) ∧ . . .. This fact can be utilized by the introduction of functional simulators. Intuitively, a functional simulator F_{R} for some binary predicate R is a set of functions which covers the responsibilities of this very relation.

In fact, it is not really necessary to consider F_{R} as a set of functions, i.e. it is nowhere really required that the elements of a functional simulator do indeed have such typical properties like: two (total) functions are identical iff they have the same result on every input. It is rather recommended to view them as nothing but a new set of elements which all can be “applied” to other kind of elements. Thus, and in order to stay in first-order syntax, instead of writing: ∃f P (f(x)) we will write: ∃f P (x:f).

3.2 Application to Serial Modal Logics

In serial modal logics we get formulae of the kind ∃x R(α, x) ∧ Φ(x) after translating modal logic programs of the form ◇Φ. The alternative formula morphism which we are going to define next handles therefore exactly this situation.

Definition 5. The formula morphism ⌊Φ⌋_{u}^{⋆} which accepts a modal logic formula Φ in negation normal form^{1} and a symbol u denoting a world is exactly like ⌊Φ⌋_{u} with two exceptions, namely

\begin{aligned}⌊◇Φ⌋_{u}^{⋆} & = & ∃x_{R} ⌊Φ⌋_{u:x_{R}}^{⋆} \\ ⌊∃x Φ⌋_{u}^{⋆} & = & ∃y_{E} ⌊Φ⌋_{u}^{⋆}[x/u:y_{E}] \end{aligned}

1 A formula is in negation normal form if all the implication and equivalence signs are eliminated and all negations are put inwards as far as possible. It is evident that any formula can be equivalently transformed into its corresponding negation normal form.

This alternative translation method does not yet preserve unsatisfiablity (although it preserves satisfiability). Something is missing which we had from the relational translation and which we don’t have in this kind of translation anymore, namely the duality of □ and ◇ and the duality of ∀ and ∃. However, we certainly need these dualities and therefore we have (in addition to the axiom schemata which we get by considering special modal logics) two additional axiom schemata, namely □Φ ⇔ ¬◇¬Φ and ∀x Φ ⇔ ¬∃x ¬Φ. We cannot deal with these axiom schemata directly, however, we can try to find their respective first-order correspondences provided they exist at all. And indeed there are such characteristic correspondences, namely: ∀u, x_{R} R(u, u:x_{R}) and ∀u, v R(u, v) ⇒ ∃x_{R} u:x_{R} = v for the duality of □ and ◇ and similarly ∀u, x_{E} E(u, u:x_{E}) and ∀u, v E(u, v) ⇒ ∃x_{E} u:x_{E} = v for the duality of ∀ and ∃.

The usefulness of this result would be questionable if we had not the following theorem which states that the conditioned equations are not necessary.

Theorem 6. Let Φ be a (serial) modal logic formula in negation normal form and let Axioms be the set of clauses induced by the properties of the underlying accessibility relation (i.e. the first-order representation of the accessibility relation properties of ML as they are known from the relational translation). Then Φ is ML-unsatisfiable iff ⌊Φ⌋_{ι}^{⋆} ∧ R(u, u:x_{R}) ∧ E(u, u:x_{E}) ∧ Axioms is predicate logic unsatisfiable where Axioms are again the characteristic accessibility relation properties for the logic ML.

Proof. (Sketch; for more details see [3] and [4]) For the “only-if”-direction of the proof it first has to be shown that a suitable functional simulator can be defined. This is quite easy by showing that any serial binary relation can be split into enumerably many functional subrelations. In order to guarantee that the □ and ◇-operators are still duals (in spite of the “non-dual” translation) we have to find out what the first-order equivalent of the axiom schema □Φ ⇔ ¬◇¬Φ is and it turns out that this results in the conjunction of the unit clause R(u, u:x) with the conditioned equation R(u, v) ⇒ ∃x u:x = v (and similarly with the existence-predicate E). Thus the only thing which remains to be shown is that this conditioned equation is indeed superfluous. To this end we consider this equation as being directed from left to right (this is allowed because after skolemization the right-hand-side variables form a proper subset of the left-hand-side variables) and give it a high priority in the resolution process, i.e. paramodulation steps have higher priority than resolution steps (ordered resolution). Now the negation normal form comes into play, because it can easily be seen that if the original formula to be translated is in negation normal form then there is no application of the equation possible on the translation result. Also there is no possible application of the equation on any of the elements in Axioms. Therefore they can be applied only to R(u, u:x) (or E(u, u:x_{E}) respectively) which results in a tautology. Thus, the conditioned equations are indeed superfluous. For the right-to-left direction of the proof it is very easy to see that a fully relational model can be constructed from a translated model by adding R(α, β) for each subterm α′:β′ such that the interpretation of α in the one model is identical to the interpretation of α′ in its translation and, analogously, the interpretation of β is identical to the (translated) interpretation of α′:β′.

Thus, instead of using the full relational translation we are allowed to perform the alternative version which is much more compact provided we add the single unit clause R(u, u:x_{R}) (and also maybe E(u, u:x_{E}) if we consider varying domains) to the program clauses. What indeed has been gained is stated in the following lemma.

Lemma 7. Let Φ be a set of modal Horn formulae in negation normal form and let Ψ be exactly like Φ if we ignore the modal operators. Then

– ⌊Φ⌋_{ι}^{⋆} contains exactly as many clauses as Ψ

– ⌊Φ⌋_{ι}^{⋆} is Horn iff Ψ is Horn

Proof. Simple induction over the structure of Φ.

3.3 Application to Sorted Logic

Definition 3 already gives us a hint how the functional simulation approach can be applied to sorted logics as well. Here we have an auxiliary binary predicate S which can only occur in the form we require (note that in analogy to modal logics we have to assume that sorts are always non-empty). Thus we are allowed to change the relational translation accordingly to:

⌈∃x: A Φ⌉^{⋆} = ∃y ⌈Φ⌉^{⋆}[x/a:y]

where the other possible cases remain as in Definition 3. By the same argument as for the application to modal logics we still have to guarantee the ∀–∃–duality and we do this by adding the unit clause S(u, u:x) (note that here as well the other direction of the duality, namely the conditioned equation, is again superfluous provided the formula to be translated is in negation normal form). Thus we have:

Theorem 8. Let Φ be a sorted logic formula in negation normal. Then Φ is (sorted logic–)unsatisfiable iff ⌈Φ⌉^{⋆} ∧ S(u, u:x) is predicate logic unsatisfiable.

Proof. Analogous (and even simpler) to the proof above.

What we gain from this translation is, in analogy to modal logics, a reduction in the number of generated clauses and, also, that the result is Horn if the sorted program was Horn (modulo sort declarations). We fix this by the following lemma:

Lemma 9. Let Φ be a set of sorted Horn formulae in negation normal form and let Ψ be exactly like Φ if we ignore the sort restrictions on variables. Then

– ⌈Φ⌉^{⋆} contains exactly as many clauses as Ψ

– ⌈Φ⌉^{⋆} is Horn iff Ψ is Horn

Proof. Simple induction over the structure of Φ.

4 (Partial) Saturation

What is remarkable about the alternative translation is not only that it does not increase the number of clauses or that it keeps the Horn structure of formulae but also that it results in clauses in which the auxiliary predicate symbol occurs only negatively. Thus the only positive occurrences of such an auxiliary predicate symbol are in the background theory, i.e. either in the unit clauses R(u, u: x_{R}), E(u, u: x_{E}) and S(u, u: x) which stem from the duality schemata or in the additional Axioms which describe the modal logic accessibility relation properties or the subsort relationships. In particular in the case of modal logics it can be shown that this can be utilized in a way which sometimes significantly simplifies this background theory.

The idea of this approach is to consider only this background theory, knowing that it is characteristic for the logic in question and not for the theorem to be proved.

Definition 10 (Saturation). Let C be a set of clauses and let P be a designated predicate symbol which occurs positively in each of the elements of the clause set. Then we call the clause set which we can get by resolution in C and whose elements do not contain any negative occurrence of P the saturation of C with respect to P.

As a little example consider the clause set {P (a), ¬P (x) ∨ P (f(x))}. Its saturation obviously is: {P (f^{n}(a)) | n ≥ 0}.

Knowing about the saturation of a given clause set is often quite helpful as the following lemma states.

Lemma 11. Let C be a clause set and let P be a designated predicate symbol. Moreover let C′ ⊆ C be exactly the subset of C which contains P positively and let C′′ be the saturation of C′ with respect to P. Then C is unsatisfiable iff C \C′ ∪C′′ is unsatisfiable.

Proof. Easy by definition of saturation.

The problem with the above lemma is that saturations are usually infinite. However, if we are able to find a finite alternative clause set with exactly the same saturation we can use this one instead.

Theorem 12. Let C be a finite clause set, P be a designated predicate symbol, C′ ⊆ C be exactly the subset of C which contains P positively and C′′ be a finite set of clauses whose elements have a positive occurrence of P and whose saturation with respect to P is identical to the saturation of C′ with respect to P. Then C is unsatisfiable iff C \ C′ ∪ C′′ is unsatisfiable.

Proof. Follows directly from the lemma above.

Thus the idea is to extract C′ and to find a hopefully simpler clause set C′′ with the same saturation.

4.1 Application to serial modal logics

Recall that the translation of an arbitrary set of (Horn) clauses results in a clause set which contains no positive R- or E-literal at all. Therefore the only positive occurrences are within the background theory given by the two duality unit clauses and the accessibility relation properties (and also maybe the domain properties). It is thus evident that this background theory is a wonderful candidate for the clause subset to be extracted and that in particular because this background theory is characteristic for the logic in question and not the theorem to be proved.

Up to now the saturation of quite a lot of modal logics have been examined in order to find suitable simpler alternatives. We won’t go into detail for each of these logics but simply summarize the results in a table (the interested reader is again referred to [4] and [3]).

Logic  Axioms  Alternative
KD  R(u, u:x)  R(u, u:x_{R})

KT  \begin{matrix}R(u, u:x) \\ R(u, u) \end{matrix}  \begin{matrix}R(u, u:x_{R}) \\ R(u, u) \end{matrix}

KDB  \begin{matrix}R(u, u:x) \\ R(u, v) ⇒ R(v, u) \end{matrix}  \begin{matrix}R(u, u:x_{R}) \\ R(u:x_{R}, u) \end{matrix}

KD4 \begin{matrix}R(u, u:x) \\ R(u, v) ∧ R(v, w) ⇒ R(u, w) \end{matrix} \begin{matrix}R(u, u:x_{R}) \\ R(u, v) ⇒ R(u, v:x_{R}) \end{matrix}

S4 \begin{matrix}R(u, u:x_{R}) \\ R(u, u) \\ R(u, v) ∧ R(v, w) ⇒ R(u, w) \end{matrix} \begin{matrix}R(u, u) \\ R(u, v) ⇒ R(u, v:x_{R}) \end{matrix}

KD5 \begin{matrix}R(u, u:x_{R}) \\ R(u, v) ∧ R(u, w) ⇒ R(v, w) \end{matrix}  \begin{matrix}R(u, u:x_{R}) \\ R(u:x_{R}, v:y_{R}) \end{matrix}

KD45 \begin{matrix}R(u, u:x_{R}) \\ R(u, v) ∧ R(v, w) ⇒ R(u, w) \\ R(u, v) ∧ R(u, w) ⇒ R(v, w) \end{matrix}  R(u, v:x_{R})

S5 \begin{matrix}R(u, u:x_{R}) \\ R(u, u) \\ R(u, v) ⇒ R(v, u) \\ R(u, v) ∧ R(u, w) ⇒ R(v, w) \end{matrix}  R(u, v)

As an example how these alternative are constructed we take a little closer look at the logic KD45. First recall that for any KD45 theorem to be proved the only clauses which contain positive R-literals are those of the background theory given by

R(u, u:x_{R})
R(u, v) ∧ R(v, w) ⇒ R(u, w)
R(u, v) ∧ R(u, w) ⇒ R(v, w)

The saturation of this clause set results in the (infinitly many) clauses

R(u:x_{1} ⋯:x_{n}, u:y_{1} ⋯:y_{m})

where n ≥ 0 and m ≥ 1. Now note that for each world it can be assumed that it is accessible from the initial world by finitely many R-steps (generatedness of models). In our terminology this means that any u can be represented by a term of the form ι:z_{1} ⋯:z_{k} with k ≥ 0. Therefore we have as a special case from above that

R(ι:x_{1} ⋯:x_{n}, ι:y_{1} ⋯:y_{m})

and thus R(u, v:x) for any worlds u, v and functional simulator element x since ι:x_{1} ⋯:x_{n} and ι:y_{1} ⋯:y_{m−1} represent arbitrary worlds.

The table can be read as follows: given the alternative translation and a modal logic: instead of using the characteristic Axioms of this logic include the usually simpler alternative form and you lose neither satisfiablity nor unsatisfiablity.

Similarly, the whole approach of saturation can also be applied to varying domains. In this case one has (besides the duality axiom E(u, u:x_{E})) also clauses which state for example that the domains are increasing, decreasing or identical. The respective results are tabled as well.

Increasing Domains

KD KD4 S4 \begin{matrix}E(u, u:y_{E}) \\ E(u, x) ⇒ E(u:y_{E}, x) \end{matrix}

{KD5 \atop KD45}  \begin{matrix}E(u, u:y_{E}) \\ E(u:x_{R}, v:x_{E}) \end{matrix}

Decreasing Domains

KD KD4 S4 \begin{matrix}E(u, u:y_{E}) \\ E(u:x_{R}, y) ⇒ E(u, y) \end{matrix}

{KD5 \atop KD45}  \begin{matrix}E(u, u:y_{E}) \\ E(u, v:x_{R}:y_{E}) \end{matrix}

5 Examples

5.1 Modal Logics

Let us consider the example 1 on page 4 which inevitabely runs into an endless loop after relational translation. Functional Simulation translates the program ◇□◇P ⇒ ◇P into

P (u:f(u)) ⇐ R(ι:a, u).
R(u, u:x).
R(u:x, u).
⇐ P (v), R(ι, v).

Thus there are no more loops and Prolog runs without any problems.

Now let us have a look at a more complex example: the Red Hat Puzzle. Assume three people are sitting in a row and there are three red hats and two blue ones and each of these people wears a hat which s/he can’t see. The first person (who sees both of the others) is asked whether s/he knows the colour of her/his hat and s/he admits that s/he doesn’t know it. The same happens with the second person (who sees only the one in front of her/him). Then the third person (who doesn’t see anyone of the others) knows that s/he got a red hat. Why?

What we need here is actually a multi modal logic, i.e. we need several modal operators, one for each person and one for their mutual belief. This certainly increases complexity but causes no particular problems. For more information see again [3]. For our example we consider the belief modalities □_{A}, □_{B}, and □_{C} for the three people and □_{MB} for their mutual belief. As a belief theory we choose KD45, i.e. beliefs are assumed to be consistent and the agents have complete introspection. Recall that the KD45 background theory can be represented by a single unit clause for each agent, namely R_{x}(u, u:y_{x}). Furthermore there is also a single unit clause necessary for the mutual belief (R_{MB}(ι, u:y_{x}))^{2}. The puzzle can then be represented by the following modal logic formulae:

□_{MB}(□_{A}red(B) ∨ □_{A}¬red(B))
□_{MB}(□_{A}red(C) ∨ □_{A}¬red(C))
□_{MB}(□_{B}red(C) ∨ □_{B}¬red(C))
□_{MB}(¬(□_{A}red(A) ∨ □_{A}¬red(A)))
□_{MB}(¬(□_{B}red(B) ∨ □_{A}¬red(B)))
□_{MB}(red(A) ∨ red(B) ∨ red(C))
□_{MB}(□_{x}red(y) ⇒ red(y))

2 This might require some further explanation. We interpret a mutual belief as: each agent believes and also each agent believes that each agent believes and so on. In our terminology this means that regardless how many (agent’s) steps are gone, the resulting world is still reachable from the initial world by the mutual belief relation. We do only have to consider the worlds accessible from the initial world since the mutual belief operator will only be put at the beginning of formulae, i.e. the agents do not reason about mutual belief.

where the top three of these formulae represent the facts that A and B know the colour of C and, additionally, that B knows the colour of C by saying that e.g. A knows whether B’s hat is red^{3}. The next two formulae state that neither A nor B know their own colour and the sixth formula represents that at least one of the three hats is indeed red. From these six statements is does not yet follow that C knows her/his colour. Note that we do not assume reflexivity for the respective accessibility relations; and indeed such an infallibility property seems to be too strong for our purpose. Nevertheless we have to be able to guarantee that the respective agents are right in their beliefs at least what the colour of the hats of the people they can see is concerned. This is stated by the seventh formula above which tells us that whenever the agent x believes that y’s hat is red then s/he is right in this respect. Note that all formula are put in a mutual belief box because the facts of the puzzle are not only true but also known to be true and known to be known to be true and so on. The theorem to be proved then finally is:

□_{C}red(C)

Unfortunately there is a non-Horn formula, however, since we know that “not red” means the same here as “blue” we can easily make it Horn and finally get as a Prolog program:

blue(u:a_{A}(u), A) ⇐ R_{MB}(ι, u).
blue(u:c_{B}(u), B) ⇐ R_{MB}(ι, u).
blue(e_{C}, C).
blue(u:k_{x}(u), y) ⇐ blue(u, y), R_{MB}(ι, u).
blue(v, B)  ⇐ R_{A}(u, v), R_{A}(u, w), R_{MB}(ι, u), blue(w, B).
blue(v, C)  ⇐ R_{A}(u, v), R_{A}(u, w), R_{MB}(ι, u), blue(w, C).
blue(v, C)  ⇐ R_{B}(u, v), R_{B}(u, w), R_{MB}(ι, u), blue(w, C).
R_{MB}(ι, v:y_{x}).
R_{x}(u, u:y_{x}).
⇐ blue(u:b_{A}(u), A), R_{MB}(ι, u).
⇐ blue(u:d_{B}(u), B), R_{MB}(ι, u).
⇐ blue(u, A), blue(u, B), blue(u, C), R_{MB}(ι, u).

We fed this to Quintus Prolog and it got easily be solved in less than a millisecond. The reader interested in more details is again referred to [3].

5.2 Sorted Logics

We applied the approach to an example which is not really an example for sorted logic programs but one which to some extent implements a matrix method solution to the world famous Steamroller problem (see Stickel’s paper and Pelletier’s

3 Note that “knowing whether” is equivalent to “either knowing that or knowing that not”; and this is not the same as “either knowing or not knowing”.

Problem Corner contribution in the Journal of Automated Reasoning, volume 2, 1986). Subgoals already proved are put into a hypothesis list which gets checked for each further subgoal (either positively with success or negatively with failure). Non-Horn clauses are dealt with by adding all possible contrapositive clauses to the clause set.

Interestingly, although there are not many existentially quantified formulae occurring in this problem, it was able to solve the puzzle in less than a millisecond with Quintus Prolog on a Spark10. We also fed the problem in its functionally simulated version to the Otter theorem prover (with Hyperresolution strategy) and it showed that the number of clauses to be generated during the inference process gets reduced by a factor of 30. This shows that, although there are no saturations possible in this sorted case, the alternative translation alone suffices for a significant time saving.

6 Summary and Conclusion

We presented a translation approach from modal or sorted logic programs into classical predicate logic programs which avoids the exponential explosion which we usually get with relational translation and also avoids the necessity to be able to deal with equations or theory unification in standard logic programming. It can be viewed as a mixed approach between relational translation and the functional translation approach proposed by Hans Jürgen Ohlbach [7], Fariñas del Cerro and Herzig [2], Enjalbert and Auffray [1] and others. It guarantees that the number of clauses generated by translation does not exceed the number of clauses we would get if we entirely ignored the modal operators (or sort restrictions). However, the clauses themselves might get bigger. Moreover, its output is Horn if and only if the original clause set is Horn which is not for sure in the pure relational translation approach. One of the major improvements to the purely relational or purely functional approach lies in the possibility to optimize the theory clauses which stem from the modal logic under consideration, such that they sometimes even get more or less trivial (simple unit clauses). However, to be fair, it is not always the case that there are no more loops possible in the background theory (as the symmetry example might suggest). There still is a possibility of getting loops in the theory of S4 and KD4, although I believe that these an be avoided if the instantiation of world variables is appropriately restricted. This, however, has not been examined very deeply yet. For all the other cases such loops are impossible because the background theory results in unit clauses.

What the application of the approach to sorted logics is concerned: usually such optimizations by saturation are not possible in sorted logics simply because there are no general facts about sorts. The best we can get (and which is also used in this paper) is the assumption that sorts are not empty. The saturation approach would come into play if there were some further general information as e.g. the intersection of two sorts form another sort. Without such extra information the advantages of the approach lies only in the fact that there are less clauses than we would have after relational translation (or relativization) and that the output is guaranteed to be Horn if the input was.

Note that this approach does by no means require to change the programming language environment. It simply transforms the original problem into an equivalent one which can then be treated by standard Prolog.

References

1. Yves Auffray and Patrice Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247 – 295, 1992.

2. Luis Fariñas del Cerro and Andreas Herzig. Quantified modal logic and unification theory. Rapport LSI 293, Languages et Systèmes Informatique, Université Paul Sabatier, Toulouse, 1988.

3. Andreas Nonnengart. First-order modal logic theorem proving and standard PRO-LOG. Technical Report MPI-I-92-228, Max-Planck-Institute for Computer Science, Saarbrücken, Germany, July 1992.

4. Andreas Nonnengart. First-order modal logic theorem proving and functional simulation. In Ruzena Bajcsy, editor, Proceedings of the 13th IJCAI, volume 1, pages 80 – 85. Morgan Kaufmann Publishers, 1993.

5. Hans Jürgen Ohlbach. A resolution calculus for modal logics. In Ewing Lusk and Ross Overbeek, editors, Proc. of 9^{th} International Conference on Automated Deduction, CADE-88 Argonne, IL, volume 310 of LNCS, pages 500–516, Berlin, Heidelberg, New York, 1988. Springer-Verlag. extended version: SEKI Report SR-88-08, FB Informatik, Universität Kaiserslautern, 1988.

6. Hans Jürgen Ohlbach. A Resolution Calculus for Modal Logics. PhD thesis, University of Kaiserslautern, Germany, 1989.

7. Hans Jürgen Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.

This article was processed using the LaTEX macro package with LLNCS style