Recursive resolution for modal logic

Yevgeny Kazakov

Max-Planck-Institut für Informatik Stuhlsatzenhausweg, 85, 66123 Saarbrücken, Germany phone:+49 681-9325-223, e-mail:ykazakov@mpi-sb.mpg.de

Abstract. Resolution for the first order logic can be considered as a practical tool for obtaining a decision procedures for some theories (cf. [2]). For modal logics, however, there is no uniform formulation of the resolution principle, yet the normal modal logics are the most probable candidates to be decidable theories. The translational methods for modal logic, treated for instance in [5], yet possess some uniformness property, but does not let one to extract proofs from the refutations. On the other hand, direct methods (cf. [4], [1]) are local which gives not much practical use of them. This paper presents some arguments on generalization of the classical propositional resolution method to the language of modal logic. We give a resolution calculus for modal logic K that inherits some features of classical resolution and propose some suggestions of how can it be used for other modal logics.

1 Preliminaries

Here we start with the basic definitions for the propositional modal logic K, note some properties, define the normal forms for modal formulas and show the algorithms for transformations to these forms.

1.1 Modal logic K

We assume a usual notation for propositional modal logic: modal language consists of (countable) set of propositional variables: X_{i}, boolean connectivities: ¬ ∨ ∧ →, boolean constants: truth ⊥, false ⊤, and modal operators: □ ◇. Modal formulas can be constructed using the following grammar:

F ::= ⊥ | ⊤ | X_{i} | (¬F) | (F ∧ F) | (F ∨ F) | (F → F) | (□F) | (◇F) which means that ⊥, ⊤ and propositional variables are formulas and new formulas can be formed by using boolean connectivities and modal operators.

Propositional modal logic K, a minimal normal propositional modal logic, can be axiomatically defined as on the fig.1.1. One could give a deductive formulation for K using only the rule modus ponens, but for this purpose one needs to add an arbitrary prefix of □ in front of each axiom. We will call this system □^{n}K (see the fig.1.1). Here □^{n}A stands for \underbrace{□ … □}_{n} A. To distinguish the deriva-

tions in □^{n}K from the derivations in K we will use the respective notations:

K  □^{n}K

\underline{Axioms:}

PC Tautologies  □^{n}PC □^{n}A, were A is a tautology
N □(A → B) → (□A → □B) □^{n}N □^{n}(□(A → B) → (□A → □B))

Rules of inference: n ≥ 0

MP (A → B), A ⊢ B  MP (A → B), A ⊢ B
Nec A ⊢ □A

Fig. 1. Deductive formulations for K

A_{1}, …, A_{n} ⊢_{K} A and A_{1}, …, A_{n} ⊢_{□^{n}K} A. These formulations are equivalent: □^{n}K ⊢ A iff K ⊢ A. In addition, □^{n}K satisfies the deduction theorem:

A_{1}, …, A_{n}, B ⊢_{□^{n}K} A iff A_{1}, …, A_{n} ⊢_{□^{n}K} B → A

The idea of using resolution for some calculus can be shown as follows. While usual deductive calculus tries to find a proof for A, resolution tries to derive a contradiction from ¬A, so resolution for K should satisfy a principle:

⊢_{□^{n}K} A iff ¬A ⊢_{R} ⊥

In the scope of the deduction theorem this means that resolution calculus should be deductively equivalent to the original calculus.

1.2 Normal forms

The simple deduction algorithm needs to have a formulas in a simple form. Classical resolution for propositional logic was operated on the conjunctions of clauses, were a clause is a disjunction of propositional variables or constants or their negations. We will try to generalize this normal forms to the set of modal formulas.

We say that a modal formula is in negation normal form (NNF) if there are only propositional variables in scope of negation. Every modal formula can be transformed to an equivalent negation normal form by a simple procedure (see the fig.1.2). For example, NNF(¬□(p ∨ ◇q)) = ◇(¬p ∧ □¬q). However we can perform a further simplifications for formulas in K to form a clausal form (CF). The definition of clausal form uses a concept of modal literal and modal clause, which we recursively define as follows:

– Atoms are either propositional variables X_{i}, false ⊥ or truth ⊤.

– Modal literals are formulas of the form either a, ¬a, were a is an atom, or □C, were C is a modal clause, or ◇S, were S is a conjunction of modal clauses.

– Modal clause is a disjunction of modal literals.

Modal formula is in a clausal form if it is a conjunction of clauses. The algorithms of translating the modal formulas to their negation normal forms and clausal forms are given in the table on fig.1.2 (rules should be applied to every subformula of the formula whenever is possible). From now on we will use the following notation. The letters a, b, c, p, q, r, s, t will denote atoms, letters L, C,

\underline{⇒ NNF}  \underline{NNF ⇒ CF}
¬(A ∧ B) ⇒ ¬A ∨ ¬B (A ∧ B) ∨ C ⇒ (A ∨ C) ∧ (B ∨ C)
¬(A ∨ B) ⇒ ¬A ∧ ¬B  □(A ∧ B) ⇒ □A ∧ □B
¬□A ⇒ ◇¬A
¬◇A ⇒ □¬A

Fig. 2. Transformation rules

S perhaps with subscripts and primes will denote modal literals, modal clauses and conjunctions of modal clauses respectively (sometimes we will omit “modal” and call them just literals or clauses). We may also omit the conjunctions between clauses, assuming that S = C_{1}, …, C_{n} stands for S = C_{1} ∧ … ∧ C_{n}. In this case we may identify S with a set of clauses. We will implicitly use a “set notation” for clauses, namely we will not distinguish between different orders of literals in the clauses and we may speak about the conjunctions or disjunctions of formulas in one-element sets or empty sets, assuming that ∧{A} = ∨{A} = A, ∧{} = ⊤, ∨{} = ⊥.

Example 1. The following are clauses: □(p ∨ q ∨ ◇(r ∧ t)), ◇((p ∨ q) ∧ t) ∧ ¬p, ¬p ∨ □(□p ∨ ◇(q ∧ □r)); the following are not: (p ∨ (q ∧ r)) ∧ s, (p ∨ □(q ∧ r)) ∧ s, □(p ∨ q) ∧ ◇□((s ∨ t) ∧ q). Transformation to a clausal form:

¬□(◇p ∨ ¬◇(q ∨ (r ∧ ◇p))) ⇒ ◇(□¬p ∧ ◇(q ∨ (r ∧ ◇p)))  (NNF)
⇒ ◇(□¬p ∧ ◇((q ∨ r) ∧ (q ∨ ◇p)))  (CF)

The last formula can be also written as ◇(□¬p, ◇(q ∨ r, q ∨ ◇p)).

2 Resolution calculus

As was mentioned before, given a candidate formula A the resolution procedure should try to infer a contradiction from the negative assumption about A. If the contradiction in some form will be obtained, it is said that the negative assumption is refutable, from what follows that A is derivable. The resolution calculus for K that will be given here, saturates the clausal normal form of ¬A in order to obtain a set of clauses, containing ⊥. The variant of this resolution calculus was initially proposed in [4]. It was formulated by means of the inference system for statements of the form Σ(A, B) → C, or Γ (A) → C, which have a meaning of resolution rules. As soon as the appropriate resolution rule is inferred in this calculus, it applies to the set of clauses. This resolution system was proved to be refutationaly complete w.r.t. K which means in this context that A is derivable in K iff the empty clause can be obtained from CF (¬A) by applying rules derivable in this calculus. In contrast to this system, in our formulation we will try to perform saturation another way round: by applying resolution rule without knowing it explicitly matching the input to some number of cases and recursively executing other resolution rules.

Deduction rules:

L1. a,¬a →_{D} ⊥;
L2. □C_{1}, □C_{2} →_{D} □C if C_{1}, C_{2} →_{D} C;
L3. □C_{1}, ◇(C_{2}, S) →_{D} ◇(C, C_{2}, S) if C_{1} ,C_{2} →_{D} C;
C1. C_{1} ∨ L_{1}, C_{2} ∨ L_{2} →_{D} C_{1} ∨ C_{2} ∨ L if L_{1}, L_{2} →_{D} L;

Simplification rules:

1. C ∨ ⊥ →_{S} C;
2. C ∨ L ∨ L →_{S} C ∨ L;
3. C ∨ ◇(⊥) →_{S} C;
4. C ∨ □C_{1} →_{S} C ∨ □C′_{1} if C_{1} →_{S}^{∗} C′_{1};
5. C_{1} ∨ ◇S →_{S} C_{1} ∨ ◇S′ if S ⇒^{∗} S′;

Saturation rules:

1. S, ⊥ ⇒ ⊥;
2. S, C_{1} ⇒ S, C if C_{1} →_{S}^{∗} C;
3. S, C_{1}, C_{2} ⇒ S ,C_{1}, C_{2}, C if C_{1}, C_{2} →_{D} C;

Fig. 3. Resolution calculus RK

Formally, resolution system RK consists of three types of rules: deduction rules, simplification rules and saturation rules. Deduction rules have a form L_{1}, L_{2} →_{D} L or C_{1}, C_{2} →_{D} C, which means that they are applied either to literals or to clauses. Simplification rules C_{1} →_{S} C_{2} work on clauses and saturation

rules S_{1} ⇒ S_{2} on the set of clauses. C_{1} →_{S}^{∗} C_{2} and S_{1} ⇒^{∗} S_{2} denote the transitive closures of respective relations. Most of the resolution rules has conditions which mean that the rule can be applied whenever the conditional rule can be applied.

Given a set of clauses S one tries to find a saturation of S – a set that cannot be saturated any further. To saturate S means try to perform one of the saturation rules consequently (in a given priority) which will recursively call some other rules. In each recursion step the objects can become only “simpler”, so the process of saturation will finally terminate. Thus, RK gives a decision procedure for K.

Example 2. Suppose we want to check whether K ⊢ □(¬□p ∨ □(p ∧ q)). The negation of this formula has a clausal form: S = ◇(□p, ◇(¬p ∨ q)) Try to saturate S. Rule 1 cannot be applied since there is no ⊥ in S, rule 2 gives us a task to simplify the clause C = ◇(□p, ◇(¬p ∨ q)) There is only simplification rule 5 possible to apply, by which we should saturate S_{1} = □p, ◇(¬p ∨ q) The saturation of the set {S_{3}} = ¬p∨q is no longer possible, so we should apply the saturation rule 3 for S_{1}:

C_{1} = □p, C_{2} = ◇(¬p ∨ q) Again only one deduction rule is possible to apply, by which we resolve the literals L_{1} = □p, L_{2} = ◇(¬p ∨ q) Applying L3 we get C′_{1} = p, C′_{2} = ¬p ∨ q which can be resolved by C_{1} and L_{1} and will produce the clause C′ = q. Getting all this back, we have performed one recursive resolution step with S and saturated it to S′ = ◇(□p, ◇(¬p ∨ q), ◇(q, ¬p ∨ q)) Now it can be shown that all saturations of this set finally will produce it again, so our test formula is not derivable in K.

3 Conclusions and further work

The resolution procedure RK can be seen as a generalization of the classical propositional resolution procedure. For that reason, one could try to extend the results from the propositional resolution to the modal case, namely :

1. Adapt the rules to cope with non-ground formulas and unification;

2. Perform the refinement of resolution, using well-founded orderings of modal literals and hyperresolution (cf. [3]).

We do not seek for the extension of this procedure for the other modal logics (however in [4] it was extended to modal logics Q, T, S4 and S5), since the resolution procedure for K may have enough power to cope with the other modal logics. For instance, S4 can be formulated as □^{n}S4 = □^{n}K+□^{n}T +□^{n}4, were T is a reflexivity and 4 is a transitivity axioms. Deduction theorem for □^{n}K will give us S4 ⊢ A iff □^{n}K ⊢ A_{1} ∧ A_{2} ∧ … ∧ A_{k} → A, for some A_{i} to be instances of the axioms □^{n}T and □^{n}4. The last can be represented by a finite set of nonground formulas. So, having the formulation of RK for non-ground formulas, we can treat it as a universal decision procedure for normal modal logics.

References

1. M. Abadi and Z. Manna. “Modal theorem proving.” In 8th Int. Conf. on Automated Deduction, pages 172-186. LNCS, Springer-Verlag, 1986.

2. A. Armando, S. Ranise and M. Rusinowitch. Uniform Derivation of Decision Procedures by Superposition. In Proceedings 15th Workshop on Computer Science Logic., LNCS vol. 2142, 513-527, 2001.

3. L. Bachmair and H. Ganzinger. “Resolution theorem proving.” In J. A. Robinson and A. Voronkov, editors, “Handbook of Automated Reasoning”. Elsevier, 2000.

4. P. Enjalbert and L. Farinas del Cerro, “Modal resolution in clausal form.” Theoretical Computer Science, 65(1):1-33, 1989.

5. H.J. Ohlbach. “Translation methods for non-classical logics – an overview.” Bulletin of the Interest Group in Propositional and Predicate Logics (IGPL), 1(1):69– 90, 1993.