We present design and implementation of a system that tries to automatically determine the subset relation between two given axiomatizations of almost arbitrary propositional modal logics, which is an open challenge problem for automated theorem proving. A test suite shows that relatively simple strategies can lead to satisfactory results, but also that certain subproblems are hard for current automated theorem provers.
Plain propositional modal logic is standard knowledge (see, e.g., [HC96]). However, there is a fundamental problem that has not been addressed in a focussed way, namely the automated decision whether among two given axiomatizations one is weaker or stronger than the other one. For example, the Modal Logic $ 100 Challenge ( [Sut]) calls for a program that can answer this problem for the most common Hilbert-style axiomatizations of K, T, S1, S1 0 , S3, S4 and S5 (see [Hal] for an overview and a list of references to various modal logics and axiomatizations).
In general, this problem is undecidable (see [HV89] for an example). But decidability can be established separately for lots of modal logics (e.g., [HM92]), e.g., using a complete Kripke semantics ( [Kri63]) and methods like filtration ( [Lem66]). There is a variety of implementations (see, e.g., [HS00], [GTG02]) of theorem provers for specific modal logics.
However, such separate implementations are relative to a specific modal logic. Sometimes the set of axioms can be varied, in particular by imposing additional restrictions on the used Kripke frames like reflexivity and transitivity. But we are not aware of a modal theorem prover permitting an arbitrary set of inference rules. Furthermore, to decide whether two distinct axiomatizations generate the same logic, a decision procedure for that logic is difficult to use since it is not always clear which derived rules it uses implicitly. Also, checking the subset relation between modal logics requires to derive rules whereas theorem provers focus on deriving axioms.
The presented work describes a general approach to the above-mentioned challenge problem. We provide a modular framework into which different strategies can be plugged in. Thus incomplete strategies covering different cases can be combined. Experimental results show that in certain cases, this works surprisingly well and identify the subproblems that still present the greatest challenges.
Sect. 2 gives the main definitions, Sect. 3 and 4 describe the currently implemented strategies, Sect. 5 introduces the system, and Sect. 6 analyzes its current and potential future strength.
We encode modal logic in first-order logic, i.e., every modal formula is a first-order term. We use the following symbols for the first-order meta logic: ∀, ∃, ¬, ∧, ⇒, . =. The theory T of first-order logic with equality is defined as follows:
• primitive function symbols or (disjunction, binary), not (negation) and box (necessity, both unary),
• further function symbols and (conjunction), imp (implication), eqv (equivalence), simp (strict implication), seqv (strict equivalence, all binary) and dia (possibility, unary) along with equality axioms that (classically) define these symbols in terms of the primitive ones, in particular strict implication and strict equivalence as
-∀x, y seqv(x, y) .
= and(box(imp(x, y)), box(imp(y, x))),
• a unary predicate symbol p (expressing provability).
A modal formula is a term of this first-order language, in particular propositional variables of modal logic are identified with first-order variables, and henceforth, just called variables. Provability of f (X) is encoded as ∀X p(f (X)) (see below for the implicit use of uniform substitution). Here, and throughout the paper, X abbreviates x 1 , . . . , x m .
Figure 1: Encoding of K Furthermore, we define:
• A rule is an additional axiom for T that is in Horn form and does not contain equality. In other words, the rule scheme
If n = 0, the rule is called an axiom.
• A modal logic is an extension of T with a finite set of rules.
• A theorem of the modal logic L is a formula f (X) such that ∀X p(f (X)) is a consequence of L. We write this as f ∈ L.
• A modal logic M is a subset of the modal logic L, written M ⊆ L, iff all theorems of M are theorems of L.
As an example, Fig. 1 gives the common and the encoded axiomatization of the modal logic K. Let U S be the rule of uniform substitution, i.e., substitution of all occurrences of a variable with the same modal formula. Then the above encoding is sound in the following sense: If L is a modal logic in our sense arising as the encoding of a Hilbertstyle set S of axioms and rules and if f is the encoding a modal formula φ, then f ∈ L iff φ is a theorem of S ∪ {U S}.
We only consider modal logics with the following two properties. Firstly, the set of theorems is closed under uniform substitution. This is fundamental for the soundness of the above encoding. We do not know of any used modal logic that does not have this property.
Secondly, the set of theorems contains all classical propositional tautologies. This assumption is connected to a principal simplification of the challenge problem: We do not assume specific, let alone minimal axiomatizations for the propositional part. This greatly increases performance without dropping too much of the original challenge. In fact, it can be argued that proving propositional theorems from specific axiom sets should be another challenge independent from the modal logic challenge (see for example the problems in the Logic Calculi domain of TPTP ([SS98])). Furthermore, there is no discussion which propositional formulas are considered theorems (except for intuitionistic logic, but all modal logics considered in the challenge are classical) so that the choice of axioms becomes just a matter of implementation. For modal logic on the contrary, there are different applications and interpretations that naturally lead to different and not necessarily equivalent axiomatizations.
The most straightforward approach would be to let a first-order theorem prover prove the inclusion directly, e.g., by renaming the predicate p to q in one of two modal logics, say L p and L q and then trying to prove ∀x(p(x) ⇒ q(x)), which corresponds to L p ⊆ L q . This is far from possible. Instead we break the problem down into subproblems treating every rule of L q separately. The resulting problems can be attacked by existing tools.
In the sequel, we present simple criteria how to do that. These criteria are not necessarily complete and cover different situations. For the remainder of this section, let L and M be modal logics and let M ′ be as M but with an additional rule r.
Let n = 0, i.e., r is an axiom, say r = ∀Xp(c(X)). Clearly, we have
This criterion can be used quite well by theorem provers. It can fail if r is complex. The following more sophisticated criterion using relational semantics and correspondence results can be applied less often but is successful in some cases in which Lem. 1 fails in practice.
Lemma 2. Let 1. L be normal, i.e., K ∈ L and L is closed under MP (modus ponens) and N (necessitation) (see Fig. 2 for the formulas; most of the time we use the same names as [Hal]), 2. F be a set of axioms of L that are Sahlqvist formulas, 3. P be the first-order property of Kripke frames completely characterized by F , 4. c ′ be the standard first-order translation of the modal formula c by making worlds explicit, 5. c ′ be first-order provable from P .
Then c ∈ L.
By standard first-order translation, we mean the relational semantics of modal logics, e.g., P is translatated to ∀w∀x(Acc(w, x) → P (x)) for an accessibility realtion Acc.
This result is due to Sahlqvist [Sah75]. Lots of practically relevant axioms are Sahlqvist formulas, e.g., any formula of the form A → B where B is a positive formula and A is constructed by applying conjunction, disjuncton and possiblity to boxed atoms and negative formulas. P can be computed from F using the SCAN algorithm ([GO92]) for second-order quantifier elimination, for which an implementation is available. We are currently working on implementing this strategy, so far only the special case where P does not exclude any Kripke frames is used.
Note that we cannot use relational semantics in general since Kripke semantics may be not sound (e.g., for S1) or not complete (see, e.g., [Tho74]) for a given modal logic. It is necessary to find a set of Kripke frames that corresponds to the modal logic and show that this set of frames is complete for it. The above criterion gives the most important class of modal logics where this has been done. If r is not an axiom, the situation is more complicated. The obvious naive approach is given by
∀X, Y p(simp(and(X, simp(X, Y )), Y )) H3
∀X, Y, Z p(simp(and(and(Z, X), not(and(Y, Z))), and(X, not(Y )))) H4
∀X p(imp(not(dia(X)), not(X)))
Figure 2: Rules
The opposite direction does not hold making this criterion incomplete. Essentially, two things can go wrong.
Firstly, deriving r from L means to show that whenever L contains instances of the hypotheses of r, it also contains the appropriate instance of the conclusion. The necessary and sufficient condition, however, is that whenever M ′ contains instances of the hypotheses, then L contains the appropriate instance of the For a trivial example, let M be empty, r be the rule ∀x(p(x) ⇒ p(not(x))), and L be any consistent non-empty modal logic. Clearly r is not derivable from L, but M ′ is empty (An axiomatization without axioms has no theorems.) and therefore, a subset of L.
Secondly, even if the opposite direction holds, Lem. 3 may be ineffective in practice, namely if r is only admissible in M but not derivable. For a simple special case of that, the following lemma gives an inductive admissibility criterion.
Lemma 4. Let r be of the form ∀x(p(x) ⇒ p(f (x))) for some formula f in one variable.
• for every rule of L with hypotheses h 1 , . . . , h n and conclusion c,
This can be proven by a straightforward induction over the theorems of L (The second assumption is just what is needed to make the induction step.). The most important application is the case where f (x) = box(x), i.e., where r is the necessitation rule.
Not all rules of modal logics can be easily encoded in the above way since some rules have complicated side conditions. The most important examples are (We refer to rules by abbreviations of their names, see Fig. 2 for the definitions.)
• substitution of strict equivalents (EQS): if f and seqv(a, b) are theorems then f ′ which is as f but with a subformula a replaced with b is a theorem,
• propositional necessitation (Ga): if a is a theorem with no occurrences of box or dia, then box(a) is a theorem.
It is reasonable to assume that any meta-language allowing for a natural encoding of these rules will be so strong that efficient automated solutions are unlikely. Instead we use Lemma 5. If M contains the rules SMP, AD, M1, M2, M4 and M5, then M enriched with EQS has the same theorems as M enriched with the following rules:
• ∀x, y, z(p(seqv(x, y)) ⇒ p(seqv(or(z, x), or(z, y)))),
• ∀x, y, z(p(seqv(x, y)) ⇒ p(seqv(or(x, z), or(y, z)))),
• ∀x, y(p(seqv(x, y)) ⇒ p(seqv(not(x), not(y)))),
• ∀x, y(p(seqv(x, y)) ⇒ p(seqv(box(x), box(y)))),
• ∀x, y((p(x) ∧ p(seqv(x, y))) ⇒ p(y)).
This can be proven by using the assumptions made about M (without EQS) to show that strict equivalence is a congruence relation in M . That is equivalent to M being closed under EQS (see [Por80], [Tho68]). This lemma covers the most important case, in which EQS occurs, namely Lewis's family S1 to S5 ( [Lew18]). In other cases, we are not able to express EQS.
A similar criterion for Ga is more complicated. While the necessary axiomatization of a further predicate prop that expresses the side condition is trivial, this predicate would not be preserved under uniform substitution and therefore, cannot be used. Instead a second sort, say s 2 , with function symbols for propositional logic must be used along with with a predicate symbol t and an axiomatization such that ∀X : s 2 . t(f (X)) expresses that f is a propositional tautology. Furthermore, a function symbol i : s 2 → s 1 and axioms of the form ∀x 1 , x 2 : s 1 , y 1 , y 2 : s 2 . (i(y 1 ) = x 1 ∧ i(y 2 ) = x 2 ) ⇒ i(and 2 (y 1 , y 2 )) = and(x 1 , x 2 ) are necessary.
If all previous definitions are appropriately extended to this more general setting, we have Lemma 6. If L has all propositional tautologies as theorems, then L enriched with Ga has the same theorems as L enriched with the rule ∀y : s 2 .(t(y) ⇒ p(box(i(y))).
Currently, this is not supported by the implementation.
The simplest approach to disprove a subset relation M ⊆ L is to use a first-order model finder to show that a theorem of M does not follow from L. Lemma 7. If f is a theorem of M , and if there is a first-order model for L enriched with ∃X¬p(f (X)), then M ⊆ L. This approach is essentially the same as using matrix models for modal logics (see, e.g., [McK41]). It is not complete since only finite models can be checked, but this is often sufficient in practice.
Kripke models provide another strong criterion. It is clearly not complete but successful in many cases. The idea of this approach is to find a Kripke model m ′ = (U, R, α) such that the formulas satisfied by m ′ include the theorems of L but not f for some f ∈ M ; here U is the set of worlds, R the accessibility relation, and α an assignment of truth values to the variables of f . Firstly, m ′ must satisfy all rules of L, i.e., an instance of the conclusion of a rule holds in all worlds whenever the appropriate instances of all hypotheses of the rule hold in all worlds. And secondly m ′ must satisfy not(f ) in one world.
Implementing that is less trivial than it sounds. If Kripke semantics is used to translate modal logic to first-order logic, the possibility to quantify over all formulas is lost, which is necessary to check whether a model satisfies a rule. And we are not aware of a model finder for (monadic) second-order logic. To circumvent this problem, we fix the number of worlds in U , say n, and proceed as follows.
We search for a first-order model m, from which m ′ can be generated. The signature for m contains constants 1, . . . , n (intended semantics: one constant per world of U ), the constant t (intended semantics: truth value of truth; we use any of the worlds as the truth value for falsity), and the binary predicate Acc (intended semantics: the accessibility relation R). m must satisfy that all worlds are different from each other and from t. Furthermore, the signature contains one constant x i for every variable x occurring in f and for every i = 1, . . . , n (intended semantics: x i gives the value of the assignment α to x in world i).
Let • be the following translation from the language over T to this new signature:
• the meta language connectives ∧ and ⇒ remain unchanged,
where f (X)(i) is given by the remaining cases,
and accordingly for the other propositional connectives,
Here, the intended semantics of ∀X p(f (X)) is that f holds in all worlds of m ′ and that of f (X)(i) is that f holds in the world i. Then the needed requirements for m are that it satisfies r for all rules r of L and not(f (X))(1). These requirements can be sent to a first-order model finder. From the generated model m, m ′ is constructed by • U : the universe of m minus the interpretation of t,
• R: the restriction of the interpretation of Acc to U ,
and it is false otherwise.
Lemma 8. If f is a theorem of M and there is an n such that a model for L and not(f ) as described above can be found, then M ⊆ L.
The follows directly from the above construction.
The implementation of the presented criteria was done in SMLNJ ( [SML]) and is available as [Rab]. It requires binary files for Vampire ( [RV02]) and Paradox ( [CS03]) to be present in the current directory because these are invoked to solve the generated subproblems.
The main function is invoked as Main.compare(f1,f2) where f1 and f2 are the names of files containing the modal logics in TPTP syntax ( [SS98]). The content of the file definitions.tptp contains the propositional axiomatization and is added to each logic.
compare calls both subsumes(f1,f2) and subsumes(f2,f1). Firstly, subsumes(big,small) calls inclusion(big,small) to prove small ⊆ big. It tries all strategies given in the list incl strategies trying to derive each rule of small as a consequence of big. Proven rules are added to big. If all rules are proven, a proof object is returned, otherwise the exception fail is raised.
In the latter case, the underived rules, say l, are passed to noninclusion(big,l), which calls each disproving strategy given in the list nonincl strategies with each element of l. If a counter-example is found a proof object is returned. compare collects these results and outputs the final result.
Optionally, whenever an external call is carried out the user is prompted for confirmation. It is possible to skip a call and choose whether the program should assume that the call has succeeded or failed.
Criterion Strategies are functors that take a prover (or model finder) as an argument. Each strategy implements a sufficient criterion and tries to establish it by calling the prover. The provers are wrapper structures that invoke external first-order tools.
Strategies and provers are designed to be modular, which makes it easy to add further strategies and provers in the future. Currently only a minimal set of strategies is implemented, see Fig.
The 100 $ challenge mentions eight logics with a total of about 25 axiomatizations that can be expressed in our encoding. This leads to about 600 combinations of logics. Fig. 4 shows the experimental results for a set of six examples. Running the program partially for other cases showed that this set is fairly representative for difficult instances. Here, the relationship between the logics (fifth column) is Log1 R Log2 where R ∈ {⊂, ⊃, = , =}. The program's answer R ′ is given in the sixth column: For partial success of the search, R ′ can also be in {⊆, ⊇, ⊆, ⊇, −}. The symbol = denotes incomparability, and − denotes complete failure. Note that the strategies Containsk and Naivemodelwere not used for this test.
As can be seen, none of the cases could be solved completely. The seventh column gives the problems with positive criteria, which consisted of rules that could not be proven although they were provable. The eighth column gives the problems with negative criteria, which occurred only in one case where the used criterion was incomplete.
Comparing the run time shows that if a relation could be determined, this was done relatively fast: less than 30 minutes on a 3 GHz Intel Xeon machine. And this time was mainly spent waiting for the five-minute time limit of a failing Vampire call. Successful Vampire calls returned results within seconds, only sometimes minutes. Even more interesting, hardly any improvement could be observed by increasing Vampire's time limit: In the case of the third row, even 20 hours did not suffice to derive M5. Since M5 is a base axiom occurring in several natural axiomatizations, this becomes an interesting challenge problem for automated theorem proving. Calls to negative criteria did not contribute significantly to the run time.
This shows that the run time is essentially determined by the time limit for failing prover calls. Due to the nature of the problem, such calls occur frequently. This suggests that a more sophisticated switching between trying to prove inclusion or non-inclusion and varying the time limit for porver calls may lower the run time significantly.
The most interesting conclusion to be drawn about proving inclusion is that the complicated theoretical problems of rules that are only admissible but not derivable and of the incompleteness of the criterion in Lem. 3 are less relevant than expected: Both problems did not strike at all. All rules that could not be derived are axioms (K, M5 and M8). For these, however, the strategy Direct is complete. Apparently even a relatively small complexity of an axiom leads to de-facto unprovability.
As to proving non-inclusion, the incompleteness of the strategy Kripke hit twice: Both K and M1 to M5 hold in all Kripke models and their negation can never be satisfied. An obvious improvement of the current implementation is to apply rules that could not be derived to axioms in order to obtain more potential counter-examples. It is not clear if this will be successful in practice or if other approaches (like the recently implemented strategy Naivemodel) have to be considered.
It is not clear whether the strategy Sahlqvist obeys the spirit of the 100 $ challenge: Since it uses an external completeness result, it can be argued that the strategy uses hidden knowledge about the problems and is not a pure theorem prover. However, the performance of this strategy provides an enticing argument: Already the very special case implemented in the strategy Containsk (which does not even use the Sahlqvist results) can derive M5 in all four critical cases within seconds, and M8 can be derived by Sahlqvist. Thus, although this strategy can never help to prove K itself or nonnormal axioms, it solves the problems in the last four rows of Fig. 4.
We are bringing together different techniques to implement and integrate them into a framework directed at a specific challenge problem of theorem proving. Clearly, the current implementation is not much more than a proof of concept, but the current version already brings promising results. Implementing the algorithm of Lem. 2 fully or even partially will strengthen it significantly.
We also found that pure proof search without using semantical correspondence results seems to be practically incomplete for relevant problems. And the question how to derive non-normal axioms or K is open. However, we expect that a larger set of strategies (e.g., splitting as described in [Kra99]) will cover almost all interesting cases. Less sophisticated possible future work includes
• utilizing different provers to exploit their respective strengths,
• tweaking, dynamically assigning or iteratively increasing the search depth, which is now fixed (5 minutes for Vampire, 4 worlds for Kripke models),
• redesigning the main functions to minimize the time spent with failing calls, in particular dynamically switching between trying to prove inclusion or non-inclusion, and keeping better track of positive and negative partial results,
• parallelizing external calls.
By publishing this work in progress, we hope to gain support and feedback for the further attack of this problem.