KSP: A Resolution-based Prover for Multimodal K, Abridged Report

1 Introduction

Modal logics have long been used in Computer Science for describing and reasoning about complex systems, including programming languages [Pratt, 1980], knowledge representation and reasoning [Rao and Georgeff, 1991; Halpern and Moses, 1992], verification of distributed systems [Hailpern, 1982; Halpern et al., 1983; Halpern, 1987] and terminological reasoning [Schild, 1991]. The most basic of such logics is the multimodal Kn, which extends the classical language with new operators, □a and ♦a , with a ∈ A = {1, . . . , n}, a fixed finite set of indexes (Section 2). The local satisfiability problem for the multimodal propositional case is PSPACEcomplete [Halpern and Moses, 1992]. The global satisfiability and the local satisfiability under global constraint problems for Kn are EXPTIME-complete [Spaan, 1993]. Given the inherent intractability of the reasoning problem and also the wide range of applications to which those logics can be applied, the development of automatic, efficient tools for theorem proving is highly desirable.

Several proof methods and tools for modal reasoning exist, either in the form of methods applied direct to the modal language or obtained by translation into more expressive languages (First-Order Logic, for instance). Here we concentrate on a direct method for Kn, the modal resolution procedure described in [Nalon et al., 2015]. Resolution [Robinson, 1965] is a saturation procedure, that is, formulae which are consequence of a given input set are added to this set until a contradiction is derived or the satisfiability of the set is evident. Following successful refinements and strategies used in theorem-provers for classical logic (see [Schulz and M¨ohrmann, 2016], for instance), our calculus is designed for restricting as much as possible the number of clauses produced during saturation. In particular, we take advantage of

Ullrich Hustadt and Clare Dixon

Department of Computer Science University of Liverpool

{U.Hustadt,C.Dixon}@liverpool.ac.uk

well-known properties for the satisfiability problem for Kn, namely: a formula ϕ is satisfiable if, and only if, it is satisfiable in a finite tree-like model; and also that checking the satisfiability of a subformula associated with level ml of the tree depends only on the subformulae occurring at levels greater or equal to ml [Areces et al., 2000]. The procedure, which is presented in Section 3, requires the translation of a formula ϕ into a more expressive language, where labels are used to denote the level at which ϕ occurs. Labelled resolution is then applied in order to determine the satisfiability of ϕ.

In this paper, we briefly present KSP, a theorem prover for the basic multimodal logic Kn which implements the calculus described in [Nalon et al., 2015] as a variation of the set of support strategy [Wos et al., 1965]. The prover also implements several other refinements and simplification techniques in order to reduce the search space for a proof (Section 4). Besides the set of support strategy, all other refinements of the calculus are implemented as independent modules, allowing for a better evaluation of how effective they are. The experimental evaluation indicates that KSP works well on problems with high nesting of modal operators where the separation of modal layers can be exploited to improve the efficiency of reasoning (Section 5). An extended version of this paper can be found at [Nalon et al., 2016a].

2 Language

Let A = {1, . . . , n}, n ∈ N, be a finite fixed set of indexes and P = {p, q, s, t, p′ , q′ , . . .} be a denumerable set of propositional symbols. The set of modal formulae, WFF, is the least set such that every p ∈ P is in WFF; if ϕ and ψ are in WFF, then so are ¬ϕ, (ϕ∧ψ), and □a ϕ for each a ∈ A. The formulae false, true, (ϕ ∨ ψ), (ϕ ⇒ ψ), and ♦a ϕ are introduced as the abbreviations for (ϕ∧¬ϕ), ¬false, ¬(¬ϕ∧¬ψ), (¬ϕ ∨ ψ), and ¬□a ¬ϕ, respectively (where ϕ, ψ ∈ WFF). A literal is either a propositional symbol or its negation; the set of literals is denoted by L. A modal literal is either □a l or ♦a l, where l ∈ L and a ∈ A. The literals (resp. modal literals) l and ¬l (resp. □a l and ♦a ¬l = ¬□a l) are said to be complementary. The modal depth of a formula is given by the maximal number of nested occurrences of modal operators in that formula. The modal level of a subformula is the maximal number of nested occurrences of modal operators in which scope the formula occurs. For instance, in □a ♦a p, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)

Figure 1: Inference rules, where ml = σ({ml1, . . . , mlm+1, mlm+2 - 1}) in GEN1, GEN3; ml = σ({ml1, ml2}) in LRES, MRES; and ml = σ({ml1,ml2,ml3}) in GEN2.

the modal depth of p is 0 and its modal level is 2. Formal definitions can be found in [Nalon et al., 2015].

As our calculus operates on a labelled clausal normal form that is closely linked to the tree model property of Kripke models for Kn, we briefly state the semantics of Kn. A treelike Kripke model M for n agents over P is given by a tuple (W,w0,R1, . . . ,Rn, π), where W is a set of possible worlds with a distinguished world w0, each accessibility relation Ra is a binary relation on W such that their union is a tree with root w0, and π : W → (P → {true, false}) is a function which associates with each world w ∈ W a truthassignment to propositional symbols. Satisfaction of a formula at a world w of a model M is defined by:

• 〈M, w〉 |= p iff π(w)(p) = true, where p ∈ P;
• 〈M,w〉 |= ¬ϕ iff 〈M,w〉 ̸|= ϕ;
• 〈M,w〉 |= (ϕ∧ψ) iff 〈M,w〉 |= ϕ and 〈M,w〉 |= ψ;
• 〈M,w〉 |= □a ϕ iff for all w′ , if wRaw′ then 〈M,w′ 〉 |= ϕ.

Let M = (W, w0, R1, . . . , Rn, π) be a model. A formula ϕ is locally satisfied inM, denoted byM |=L ϕ, if 〈M, w0〉 |= ϕ. The formula ϕ is locally satisfiable if there is a model M such that 〈M,w0〉 |= ϕ. A formula ϕ is globally satisfied in M, if for all w ∈ W, 〈M,w〉 |= ϕ. We denote by depth(w) the length of the unique path from w0 to w through the union of the accessibility relations in M. We call a modal layer the equivalence class of worlds at the same depth in a model.

We note that checking the local satisfiability of a formula ϕ can be reduced to the problem of checking the local satisfiability of its subformulae at the modal layer of a model which corresponds to the modal level where those subformulae occur (see [Areces et al., 2000]). Also, checking the global satisfiability of ϕ can be reduced to checking the local satisfiability of ϕ at all modal layers (up to an exponential distance from the root) of a model [Goranko and Passy, 1992; Spaan, 1993]. Thus, an uniform approach based on modal levels can be used to deal with both problems, as given in the next section.

3 ANormal Form and Calculus for Kn

The calculus operates on labelled clauses of the formml : C (literal clause), ml : l ⇒ □a l′ (positive a-clause), ml : l ⇒ ♦a l′ (negative a-clause) where ml ∈ N∪{∗}, C is a propositional clause, and l, l′ are literals. The label ml indicates the depth of the Kripke model at which the clause is true. The special label ∗ is used if a clause is true at all depths/worlds in a model and it normally only occurs in the normal form if we want to check a formula for global satisfiability. Any formula of Kn can be transformed into an equi-satisfiable set of labelled clauses. The calculus uses a simple form of unification. The partial unification function σ on sets of labels is given by σ({ml, ∗}) = ml; and σ({ml}) = ml; otherwise, σ is undefined. The inference rules (Figure 1) can only be applied if the unification on labels is defined.

We show next an example of a refutation which uses both local and global reasoning (from [Nalon et al., 2015], adapted from [Areces et al., 1999]). Clauses 1 and 2 say that a person is either female or male. Clauses 3 and 4 say that tall people have children with blond hair. The particular situation of Tom, denoted here by t0, is given in the following clauses. Clauses 5, 6, and 7 say that Tom's daughters are tall. Clauses 8 and 9 say that Tom has a grandchild who is not blond. We want to prove that Tom has a son, which appears negated in Clause 10. The refutation is given below.

1. ∗ : female ∨male
2. ∗ : ¬female ∨¬male
3. ∗ : ¬tall ∨ t1
4. ∗ : t1 ⇒ □c blond
5. 0 : t0
6. 0 : t0 ⇒ □c t2
7. 1 : ¬t2 ∨¬female ∨ tall
8. 0 : t0 ⇒ ♦c t3
9. 1 : t3 ⇒ ♦c ¬blond
10. 0 : t0 ⇒ □c ¬male
11. 1 : ¬t1 ∨¬t3 [MRES, 9, 4]
12. 1 : ¬tall ∨¬t3 [LRES, 11, 3]
13. 1 : ¬t3 ∨¬t2 ∨¬female [LRES, 7, 12]
14. 1 : male ∨¬t2 ∨¬t3 [LRES, 13, 1]
15. 0 : ¬t0 [GEN1, 10, 6, 8, 14]
16. 0 : false [LRES, 15, 5]

4 KSP

KSP is an implementation, written in C, of the calculus in Figure 1. The main loop is based on the given-clause algorithm implemented in Otter [McCune, 2007], a variation of the set of support strategy [Wos et al., 1965], a refinement

(a) KSP with different refinements

Figure 2: Benchmarking results for MQBF

which restricts the set of choices of clauses participating in a derivation step. For the modal calculus, the set of clauses is partitioned according to the modal layer at which clauses are true. For each modal level ml, a literal clause is selected and the prover tries to resolve it with either a literal clause at the same modal level or with a set of modal clauses in the previous modal level, ml - 1.

The partitioning of the set of clauses avoids unnecessary applications of the resolution inference rules. For instance, the translation of the formula ϕ = ♦a ♦a p ∧ □a ¬p without considering the modal level at which its subformulae occur results in the set:

4. t0 ⇒ □a ¬p

where t0 and t1 are new propositional symbols. Because ♦a p and □a ¬p are complementary, resolution applied to Clauses 3 and 4 results in ¬t0 ∨ ¬t1, which cannot be used to find a contradiction. In contrast, by using labels, the translation of ϕ results in the set:

As the labels indicate, Clauses 3′ and 4′ occur at different modal levels and resolution is not applied to those clauses. As another simple example, consider the formula □a □a p ∧ ♦a ♦a ¬p, whose layered normal form is given below.

As clauses 3 and 4 are at the same modal level, MRES can be applied, resulting in 0 : ¬t1 ∨ ¬t2. By an application of GEN1 to this clause and Clauses 2 and 4, we obtain 0 : ¬t0. Applying LRES to 0 : ¬t0 and Clause 1, results in 0 : false, which shows that the original formula is unsatisfiable.

Besides the basic calculus with a set-of-support strategy, the user can further restrict LRES by choosing ordered (clauses can only be resolved on their maximal literals with respect to an ordering chosen by the prover in such a way to preserve completeness), negative (one of the premises is a negative clause, i.e. a clause where all literals are of the form ¬p for some p ∈ P), positive (one of the premises is a positive clause), or negative + ordered resolution (both negative and ordered resolution inferences are performed). The completeness of some of these refinements depends on the particular normal form chosen. The prover can either perform local or global reasoning. For a comprehensive description of KSP see [Nalon et al., 2016a; Nalon et al., 2016b].

5 Evaluation

We have compared KSP with BDDTab [Gor´e et al., 2014], FaCT++ 1.6.3 [Tsarkov and Horrocks, 2006], InKreSAT 1.0 [Kaminski and Tebbi, 2013], Spartacus 1.0 [G¨otzmann et al., 2010], and a combination of the optimised functional translation [Horrocks et al., 2006] with Vampire 3.0 [Kov´acs and Voronkov, 2013]. Benchmarking was performed on PCs with an Intel i7-2600 CPU @3.40GHz and 16GB main memory. For each formula and each prover we have determined the median run time over five runs with a time limit of 1000 CPU seconds for each run. The experiments are fully described in [Nalon et al., 2016a], from where the graphs shown in this section are taken.

Our benchmarks [Nalon et al., 2016b] consist of three collections of modal formulae:

1. The complete set of TANCS-2000modalised randomQBF (MQBF) formulae [Massacci and Donini, 2000] complemented by the additional MQBF formulae provided by

(b) All provers

(a) Results for LWB

(b) Results for 3CNFK

Figure 3: Benchmarking results for LWB and 3CNFK

Tebbi and Kaminski [2013]. This collection consists of five classes, with a total of 1016 formulae, of which 617 are known to be satisfiable and 399 are known to be unsatisfiable (due to the output of one of the provers).

1. Logics Workbench (LWB) basic modal logic benchmark formulae [Balsiger et al., 2000], with 56 formulae chosen from each of the 18 parameterised classes. The median value of the maximal parameter value used for the 18 classes is 1880, far beyond what has ever been tested before. Of the resulting 1008 formulae, half are satisfiable and half are unsatisfiable by construction of the benchmark classes.
2. Randomly generated 3CNFK formulae [Patel-Schneider and Sebastiani, 2003] over 3 to 10 propositional symbols with modal depth 1 or 2. The formulae were chosen from each of the 11 parameter settings given in [Patel-Schneider and Sebastiani, 2003, page 372]. The resulting collection contains 1000 formulae, of which 457 are known to be satisfiable and 464 are known to be unsatisfiable.

Figure 2a compares the impact of different refinements on the performance of KSP on the MQBF collection. With plain KSP uses the rules shown in Figure 1, without additional refinement. With cord and negative ordered, KSP applies ordered resolution and negative + ordered resolution, respectively. The configuration negative (resp. positive) uses negative (resp. positive) resolution on a set of clauses. For all configurations, the same preprocessing techniques are used. The cord configuration offers the best performance. Ordered resolution restricts the applicability of the rules further than the other refinements. Not only is this an advantage on satisfiable formulae in that a saturation can be found more quickly, but also on unsatisfiable formulae where with this refinement KSP finds refutations much more quickly than with any of the other refinements.

Figure 2b compares the performance of all the provers on the MQBF collection. It shows that KSP performs better than any of the other provers. The classes of formulae on which KSP performs best are those where the number of propositional symbols is small and/or those symbols are uniformly distributed over a wide range of modal levels. This reduces the possibility of inference steps between modal clauses with complementary literals.

Figure 3 shows the benchmarking results on the LWB and 3CNFK collections. On the LWB collection KSP performs about as well as BDDTab, FaCT++ and InKreSAT, while Spartacus performs best and the combination of the optimised functional translation with Vampire (OFT + Vampire) performs worst. A characteristic of the classes on which KSP performs best is again that atomic subformulae are evenly spread over a wide range of modal levels.

Finally, on the 3CNFK collection, InKreSAT is the best performing prover and KSP the worst one. This should now not come as a surprise. For 3CNFK we specifically restricted ourselves to formulae with low modal depth which in turn means that the layered normal form has little positive effect.

6 Conclusions and FutureWork

KSP implements a variation of the set-of-support strategy by restricting further the application of inference rules to clauses whose literals are at the same modal level. The evaluation indicates that KSP works well on problems with high modal depth where the separation of modal layers can be exploited to improve the efficiency of reasoning.

The prover implements both local and global reasoning, and the implementation of the local satisfiability under global constraint procedure is ongoing work. We are are also working on the extension of the calculus for dealing with different modal logics. The calculi for Tn and 4n, which can be combined to provide a calculus for S4n, have already been implemented.

Several refinements and redundancy elimination techniques have been implemented. The choice of strategies and optimisations are, by now, all left to the user. The development of an "auto mode" in which the prover makes a choice of its own, based on an analysis of the given formula, is left for future work.