A Mechanisation of Classical Modal Tense Logics Using Isabelle

Jeremy E Dawson and Rajeev Goré

Automated Reasoning Project and Department of Computer Science Australian National University, 0200, Canberra

                       {jeremy,rpg}@arp.anu.edu.au

Abstract. We present an implementation of an interactive theorem prover for the basic tense logic K_{t}, and many of its extensions, using the generic proof assistant Isabelle. The novelty of the implementation is that we use a Display Logic formalism of K_{t} as opposed to a traditional Gentzen system. The prover is intended to assist in meta-theoretical studies of tense logics rather than to be a fast theorem prover. Since Display Logic is a generic way to capture multi-modal logics, our implementation can be trivially extended to handle the multi-modal logics of “time”, “knowledge”, “intentions”, “desires” and “beliefs” which are used in Artificial Intelligence research. Keywords automated deduction, hybrid logics, logics for knowledge and belief, display logic, tense logic, sequent calculus.

1 Introduction

Formal calculi for reasoning about modalities are an important part of Artificial Intelligence research where nonclassical logics are often used to model notions like time, belief and knowledge [FHMV95]. As our understanding of these calculi increases, so does our ability to model more complicated notions like Logics of Actions [Pra91] or Logics of Information Flow [BGH95] using other, more complicated nonclassical logics like Relevance Logics [AB75], Linear Logic [Gir87], or arbitrary substructural logics [DSH93]. The eventual aim is to be able to form natural hybrids from these individual logics by choosing aspects like “tense”, “resource consciousness”, “classicality” or “constructivity” as required by the complex artificial intelligence task we wish to model.

The traditional formalisation of these individual logics is via Hilbert systems since we have a very good understanding of such systems for many nonclassical logics. But Hilbert systems are notoriously bad for proof search, and such formulations are of little practical use when trying to build a working system.

More modern automated reasoning techniques like resolution are usually not applicable because non-classical logics rarely possess an analogue of “clausal normal form”. For example, there are numerous automated or semi-automated systems which handle classical tense or temporal logics in a resolution framework [MFD96], [Ohl88], [DEL90], [Cer82], but these methods do not immediately lend themselves to handle hybrids like Relevant Tense Logics or even Intuitionistic Tense Logics because it is not at all clear that resolution or translation methods can be extended to substructural logics in general.

As has been argued elsewhere [Wal89], cut-free Gentzen systems are a good formulation for “backward” or “goal-directed” proof search. But it is rare to find an “off the shelf” (cut-free) Gentzen system for the particular nonclassical logic one requires. Mechanisations of many of these logics do exist in the literature, but they are invariably for a particular logic, and do not facilitate the formation of hybrids. For example, one of the fastest automated theorem provers for tense logic and multi-modal logics is the Logics Workbench [HSZ96]. Although the Logics Workbench allows you to form multi-modal logics, it does not allow one modality to be based on S4 and another on K45.

Display logic [Bel82] is a general Gentzen-style formulation which not only captures a huge variety of logics, but which was specifically designed for the formation of hybrid nonclassical logics. Display calculi exist for Linear, Relevant, BCK, Lambek and other substructural logics [Gor98,Res98], for the logic of Relation Algebras [Gor97], and even for nominal tense logics [DG98]. All of these calculi are not only cut-free, but they are modular in that they can be easily combined to form cut-free display calculi for natural hybrid logics like Relevant Tense Logic; see [Gor98] for details. Hence a general mechanisation of display logic would allow us to capture many different logics in one uniform setting.

Here, we first learn to walk before learning to run by demonstrating that we can mechanise the displayed tense logics of Wansing [Wan94] by using Paulson’s generic proof assistant Isabelle [Pau90]. This mechanisation uses the generic character of Isabelle, so that we use δK_{t} as the “native” logic of the implementation, rather than entering δK_{t} axioms “on top of” (say) classical logic. More importantly, it is possible to obtain a vast number of extensions of displayed tense logics by encoding certain Hilbert axioms as structural rules of display logic, in a purely modular way. Thus our implementation not only caters to a vast number of tense and multi-modal logics, but it is trivially extendable to handle various other modalities to cater for “belief” or “knowledge”, as long as these modalities are based on classical modal logic. Our system therefore provides the essential ingredients for the formation of a hybrid modal or tense logic to suit your needs.

Our current implementation does not provide a decision procedure, although many of these individual logics are known to be decidable. But we are currently working on such an extension. However, the implementation has already helped with meta-theoretical studies, as demonstrated in [Gor98].

The plan of the paper is as follows. In Section 2 we define the syntax of classical modal tense logics. In Section 3 we briefly describe the classical modal display logic of Wansing. In Section 4 we briefly describe the proof assistant Isabelle. In Section 5 we explain how we captured displayed tense logics in Isabelle, explain the various Isabelle tactics which were written, and give an example of a complicated display logic proof. In Section 6 we describe how we can store certain previously proved theorems for future use in a totally general way. In Section 7 we highlight the beauty of display logic by desribing an automatic cutelimination process that converts a proof containing cuts into a cut-free proof. In Section 8 we describe future work and conclude.

2 Classical Modal Tense Logics

The formulae of our logics are built using the following BNF grammar where A and B stand for formulae and p for any primitive proposition:

A B ::= p | ⊤ | ⊥ | ◇A | □A | ♦A | ■A | ¬A | A → B | A ∧ B | A ∨ B

All the connectives except ◇, □, ♦ and ■ are the familiar ones from classical propositional logic. The formula ◇A is usually read as “sometime in the future”, ♦A as “sometime in the past”, □A as “always in the future” and ■A as “always in the past”. A good introduction to Kripke semantics for modal logics is [HC96].

Logics of knowledge and belief are obtained by using multiple modalities so that, for example, □_{i}A is read as “agent i knows that A is true” [FHMV95].

3 Classical Modal Display Logic

Display Logic [Bel82] is a powerful Gentzen formulation designed to allow the formation of hybrid logics. Its beauty is a generic cut-elimination theorem. Display logic is, unfortunately, rather an arcane methodology. It is best explained via an example which should be familiar to most readers.

Consider the equation 2x^{2} − 4 ≤ 0, familiar from high school algebra. It can be solved if we “make x the subject” by manipulating the equation as follows:

the equation (2 × x^{2}) − 4 ≤ 0
becomes  (2 × x^{2}) ≤ 0 + 4 by adding 4 to both sides
becomes  x^{2} ≤ (0 + 4)/2 by dividing both sides by 2
becomes  x ≤ \sqrt{(0 + 4)/2} by taking (positive) square root of both sides
becomes  x ≤ \sqrt{2}  by simplification (or rewriting).

Most of these manipulations are only possible because the operations come in “opposite” pairs that undo the effects of each other; namely (+, −), (×, /), (x^{2}, \sqrt{x}). Thus, the ability to “make x the subject” by using “opposite pairs” and to rewrite a term into a simpler (but equivalent) form are fundamental.

Instead of natural numbers and operators like multiplication, display logic has the following syntax. In δK_{t}, structures are built using the structural connectives I, •, ; and ∗ according to the following BNF grammar where A stands for any formula and X, Y, and later V, W and Z, stand for structures:

X Y ::= A | I | •X | ∗X | X ; Y

Note that, unlike in standard Gentzen systems, comma is not a structural connective, and no structural connective is automatically polyvalent.

A sequent is an expression of the form X ⊢ Y with X the antecedent and Y the succedent. A sequent rule is defined from sequents in the usual way with the premises above the line and the conclusion below the line.

Display Postulates^{(dp) \begin{matrix}∗X ⊢ Y \\ ∗Y ⊢ X \end{matrix}}  ^{(dp) \begin{matrix}X ⊢ ∗Y \\ Y ⊢ ∗X \end{matrix}}  ^{(dp) \begin{matrix}∗ ∗ X ⊢ Y \\ X ⊢ Y \end{matrix}}^{(dp) \begin{matrix}Z ; ∗ Y ⊢ X \\ Z ⊢ X ; Y \\ ∗X ; Z ⊢ Y \end{matrix}}^{rp(•, •) \begin{matrix}•X ⊢ Y \\ X ⊢ •Y \end{matrix}}^{(dp) \begin{matrix}X ⊢ Z ; ∗ Y \\ X ; Y ⊢ Z \\ Y ⊢ ∗X ; Z \end{matrix}}  Sample Structural Rules^{(Ass ⊢) \begin{matrix}X ; (Y ; Z) ⊢ W \\ (X ; Y) ; Z ⊢ W \end{matrix}}^{(Ass ⊢) \begin{matrix}X ; (Y ; Z) ⊢ W \\ (X ; Y) ; Z ⊢ W \end{matrix}} Sample Logical Rules (∨ ⊢) \frac{A ⊢ X B ⊢ X}{A ∨ B ⊢ X} (⊢ ∨) \frac{X ⊢ A ; B}{X ⊢ A ∨ B} (∧ ⊢) \frac{A ; B ⊢ X}{A ∧ B ⊢ X}  (⊢ ∧) \frac{X ⊢ A X ⊢ B}{X ⊢ A ∧ B} (□ ⊢) \frac{A ⊢ X}{□A ⊢ •X}  (⊢ □) \frac{X ⊢ •A}{X ⊢ □A} (◇ ⊢) \frac{• ∗ •A ⊢ X}{◇A ⊢ X}  (⊢ ◇) \frac{X ⊢ A}{• ∗ •X ⊢ ◇A}

Fig. 1. Sample Rules for δK_{t}

Thus, in Display Logic, sequents are the analogues of algebraic inequations. The display property allows us to pick any substructure X of the construct V ⊢ W, and to “make X the subject” on one side by moving all other constituents onto the other side of the turnstile ⊢. The X is said to be “displayed”. The “display property” is a by-product of special, reversible rules, called the display postulates , which allow us to unravel structures. See Figure 1.

Separate structural rules, using only structural variables like X and Y, enforce certain properties of the structural connectives like associativity (shown in Figure 1), commutativity, weakening, contraction, etc (not shown).

Finally, in Figure 1 we give a flavour of the logical rules that introduce the logical constants and the binary logical connectives into the antecedent and the succedent. Note that every introduced principal formula is “displayed”. Space forbids the inclusion of all the rules for δK_{t}, but see [Wan94] and [Kra96].

Thus the logical connectives come in pairs, with each component of a pair captured by the same structural connective, but in different (antecedent or succedent) positions. Unlike in traditional Gentzen systems, antecedent and succedent positions do not correspond exactly to left hand and right hand sides of sequents.

The display postulates allow us to dis-assemble and re-assemble any structure bigger than a formula so that any particular part of the structure can be made the whole of the antecedent, or the whole of the succedent, depending on its “polarity”. The exact side where a particular occurrence of a substructure finally rests depends upon whether it is an “antecedent part” or a “succedent part”. We formalise this as follows.

In any structure Z, the substructure X occurs negatively [respectively positively] if X appears in the scope of an odd number [zero or an even number] of ∗ connectives [Bel82]. In a sequent V ⊢ W, a particular occurrence of X is an antecedent part [succedent part] if it occurs positively in the antecedent V [positively in the succedent W] or if it occurs negatively in the succedent W [negatively in the antecedent V] [Bel82].

Two sequents s and s′ are structurally equivalent if we can pass from one to the other using only the display postulates shown above. The name Display Logic comes from the following theorem (which does not hold for subformulae!).

Theorem 1 (Belnap). For every sequent s and every antecedent/succedent part X of s, there is a structurally equivalent sequent s′ that has X (alone) as its antecedent/succedent. X is said to be “displayed” in s′ [Bel82].

Proof. By inspection of the display postulates.

Example 2. The following derivation, read upwards, shows how to display the (succedent part) B in the sequent ∗(∗A ; B) ; C ⊢ D as the whole of the succedent in A ; (C ; ∗ D) ⊢ B.

A ; (C ; ∗ D) ⊢ B (dp) C ; ∗ D ⊢ ∗A ; B

(dp) C ⊢ (∗A ; B) ; D

(dp) ∗(∗A ; B) ; C ⊢ D

Lemma 3. For any formula A, the sequent A ⊢ A is provable.

Proof. By induction on the formation of A.

The beauty of Display Logic is the following generic cut-elimination theorem.

Theorem 4 (cut-elimination). If there is a proof of the sequent X ⊢ Y, then there is a cut-free proof of X ⊢ Y (in the same display calculus) [Bel82].

Proof. The rules must obey Belnap’s conditions C1–C8 [Bel82].

4 Isabelle

Isabelle [Pau90] is an interactive computer-based proof system. It is written in Standard ML, and when it is running, the user can interact with it by entering further ML commands.

It has the unusual feature that it can be used with the user’s own choice of logical system and syntax, for very little is built in. The built-in logic is intuitionistic higher-order logic, with the operators ==> (implication, or deducibility), == (equality, or substitutibility), and !! (universal quantification). These operators have only the properties necessary to support their intended meanings. For example, since [| P; Q |] ==> R means that R can be deduced from P and Q, it follows that [| P ==> Q; P |] ==> Q, and that

            ([| P; Q |] ==> R) ==> ([| Q; P |] ==> R).

Likewise, since P == Q means that P can be replaced by Q, or vice versa, == is reflexive, symmetric and transitive. Anything that can be proved using this built-in logic is a theorem of Isabelle, of ML type thm. To avoid confusion we consistently use “thm” when speaking of Isabelle theorems and use “theorem” when speaking of the object logic K_{t}.

The user then has to define an object-level logic and syntax, though normally one would use one of several which are packaged with the Isabelle distribution. One of these is LK, which is first order logic using the Gentzen sequent calculus. In LK, ‘⊢’ is treated as an object-level operator, and object-level propositions are of the form Γ ⊢ Δ, where Γ and Δ are sequences of formulae.

Isabelle uses the strong typing of ML to prevent the user from ‘proving’ results other than by the inference steps permitted; only these steps can produce an Isabelle thm. Naturally the primitive built in inference steps can be combined, both in the more powerful functions provided in Isabelle, or by the user programming more complex proof functions in ML.

The user asserts a set of ‘axioms’ in a ‘theory file’, where the syntax of the object-logic is also specified. Isabelle treats these axioms as thms.

Isabelle thms (including the axioms of the theory) may or may not involve Isabelle’s metalogical operators. Thus, in the Isabelle implementation of Display Logic, an Isabelle thm may be either a ‘simple’ sequent of δK_{t}, of the form X ⊢ Y, or a sequent rule, such as those in Fig. 1. The uni-directional and bi-directional rules correspond to Isabelle thms containing the operators ==> (meta-implication) or == (meta-equality) respectively.

Isabelle provides a number of basic proof steps for backwards proof (tactics), as well as functions for combining these in various ways (tacticals). Isabelle automatically keeps track of the subgoals generated by this backward search procedure and the user can choose to work on any subgoal. The user can also write complex proof tactics in ML; many complex tactics and tacticals are supplied with Isabelle or its standard object logics. Some tactics are designed for a more automated style of proof search; they will repeatedly attempt a large number of tactics. Others, for example rtac, are designed more for interactive use, when the user can see what proof steps are needed. Thus rtac th sg attempts to match the conclusion of thm th to subgoal number sg – if it succeeds, it will replace that subgoal by the premises (if any) of th.

Isabelle also supports forward proof; for example, if A′==>B′ and B′′==>C′′ are thms, and the most general unifier of B′ and B′′ is θ, (so B′θ = B′′θ) then Isabelle can derive the thm A′θ==>C′′θ.

5 Capturing Display Logics Using Isabelle

The syntax of δK_{t} has been implemented in Isabelle. It uses the Isabelle type (distinct from ML types) prop (for sequents) and defines types structure and formula, so as to distinguish structure and formula variables. Since a formula can also be a structure, there is an operator “Structform”, which coerces a formula argument (of Isabelle type formula) into the “same” term, but with the type structure. Externally, at the user level, a structure variable or constant is preceded by ‘$’, to distinguish it from a formula variable.

In the Isabelle implementation, the operators are represented as follows.

δK_{t}  ; ∗ I • ∧ ∨ ¬ ⊥ ⊤ □ ■ ♢ ♦

     dKt.thy  ;  *  I  @  &  v  -  F  T  wbx  bbx  wdm  bdm

The rules have been implemented in Isabelle; the δK_{t} (⊢ ∧) rule, for example, and its Isabelle counterpart (called ands) are

\frac{X ⊢ A Y ⊢ B}{X; Y ⊢ A ∧ B}  [| $?X |- ?A; $?Y |- ?B |] ==> $?X; $?Y |- ?A & ?B

Some rules of δK_{t} can be derived from others. For example, (Ass ⊢) can be derived from (⊢ Ass). The Isabelle implementation uses this, but no effort was made to find a minimal set of rules. Some particularly useful derived rules are shown in Fig. 2. The rules andS and orA are equivalent to (⊢ ∧) and (∨ ⊢), since (⊢ ∧) and (∨ ⊢) can be derived from andS, orA and the monotonicity rules.

\begin{matrix}X ⊢ Y \\ X ⊢ ∗ ∗ Y \end{matrix} (ssS)  \begin{matrix}X ⊢ Y \\ ∗Y ⊢ ∗X \end{matrix} (dcp)

\begin{matrix}∗(X; Y) ⊢ Z \\ ∗Y; ∗X ⊢ Z \end{matrix} (cbdista)  \begin{matrix}X ⊢ ∗(Y; Z) \\ X ⊢ ∗Z; ∗Y \end{matrix} (cbdists)

\frac{(•X; •Y) ⊢ Z}{•(X; Y) ⊢ Z} (bldista)  \frac{X ⊢ •Y; •Z}{X ⊢ •(Y; Z)} (bldists)

\frac{A ⊢ X B ⊢ X}{A ∨ B ⊢ X} (orA)  \frac{X ⊢ A X ⊢ B}{X ⊢ A ∧ B} (andS)

Fig. 2. Selected Derived Rules

As in classical sequent calculus, the modus operandi for proving a sequent is to start the proof from the bottom, ie, from the goal, and work “backwards”; in terms of the written representation of proofs, that means working upwards. The first step is, where possible, to remove all the formula (logical) operators, using the logical introduction rules. In Display Logic (unlike classical sequent calculus) this requires that the formula which is to be “broken up” must first be displayed. As any formula can be displayed, this is not a difficulty, except in that it is tedious to select display postulates one-by-one. The tactics described in the next two subsections were first written to help in this style of proof.

5.1 Display Tactics

Tactics were written to help in displaying a chosen substructure. Fuller details of these are given in [DG97], and links to relevant files are at

http://arp.anu.edu.au:80/~jeremy/.

disp tac replaces a subgoal by one in which a selected structure is displayed. d b tac takes a subgoal, displays an indicated substructure, applies a tactic to

the transformed subgoal, and lastly applies the reverse of the display steps to each resulting subgoal. Since the tactic applied should change only the displayed structure, we had to derive the rules andS and orA from ands and ora for use in this style of proof. For example, if we start with the subgoal R ⊢ ((∗T; •∗S); •∗Q); Y then, using the code "-l" to denote the substructure (∗T; •∗S), d_b_tac "-l" (rtac mrs) applies the monotonicity (or weakening) rule (mrs) to the sub-structure (∗T; • ∗ S); • ∗ Q by the following steps (read upwards)

R ⊢ (∗T; • ∗ S); Y (reverse of disp tac "-l") R; ∗Y ⊢ ∗T; • ∗ S

                                     (mrs) R; ∗Y ⊢ (∗T; • ∗ S); • ∗ Q

                                     (disp tac "-l")

R ⊢ ((∗T; • ∗ S); • ∗ Q); Y

fdisp, fdispfun are functions corresponding to disp tac and d b tac, but for forward proof.

5.2 Search-and-Replace Tactics

Tactics were written to display all structures in a sequent in turn, and apply any appropriate transformations (selected from a given set) to each displayed structure. These can be used to rewrite all substructures of a particular form, for example, to rewrite all occurrences of X; (Y; Z) to (X; Y); Z.

glob tac This function displays in turn every substructure of the subgoal indicated, and applies a given tactic (if possible) to the sequent thus produced. All the display steps are eventually reversed, in the same way as for d_b_tac.

It can be used to replace any substructure of a particular form by another substructure, giving the effect of a rewrite procedure [Daw97]. glob tac uses a top-down strategy in the sense that it first looks at the whole structure, then, recursively, each sub-structure.

bup tac is like glob tac, but uses a bottom-up strategy, displaying and testing

the smallest sub-structures first. fgl fun, fbl fun These functions are like glob tac and bup tac, but for doing

forward proof.

The implementation of the search-and-replace tactics is described in [Daw97]. Examples of some of their uses are (1) to eliminate ∗∗, (2) to use the various distributive laws to push ∗ down, and (3) to eliminate logical operators, where possible, using those logical introduction rules satisfying the property that the structure on the other side is left unchanged (in backward proof only)

This last replacement is available only for backward proof because the logical introduction rules which it uses are uni-directional rather than bi-directional.

5.3 Example: proof of the K rule

In Fig. 3 we show an example of a proof in δK_{t}, using the proof of the K rule as given in [Wan94]. The rule (M ⊢) captures the monotonicity of ‘;’ and the rules (C ⊢) and (⊢ P) capture its idempotence and commutativity. (These reflect the fact that ∧ and ∨ have these properties). The notation (dp) denotes any display postulate. This proof uses the (cut) rule twice. This is the usual way of incorporating a previously proved lemma into a proof. As we see in §7, the use of the cut rule can be eliminated automatically.

6 Further Axioms as Structural Rules

It is well known that further Hilbert axioms can be added to K_{t} to capture corresponding classes of Kripke frames [Kra96]. For example the axioms T: □A → A, D: □A → ◇A, 4: □A → □□A, 5: ◇□A → □A and B: A → □◇A correspond to the conditions of reflexivity, seriality, transitivity, euclideaness and symmetry. Kracht [Kra96] has shown that we can augment δK_{t} with such axioms by adding them as structural rules, and retain soundness, completeness and cutelimination. For example, the rules shown below capture these axioms exactly:

(T) \frac{•X ⊢ Z}{X ⊢ Z}  (D) \frac{∗ • ∗I ⊢ Z}{I ⊢ Z}  (4) \frac{•X ⊢ Z}{• • X ⊢ Z}

(5) \frac{∗ • ∗X ⊢ Z}{• ∗ • ∗ X ⊢ Z} (B) \frac{∗ • ∗(∗ • ∗X; Y) ⊢ Z}{X; ∗ • ∗Y ⊢ Z}

Consequently, we can trivially extend δK_{t} and hence our implementation, to capture many extensions of the tense logic K_{t}(see [Kra96]).

\begin{matrix}\begin{matrix}A → B ⊢ A → B & (□ ⊢) & □(A → B) ⊢ •(A → B) \\ (M ⊢) \\ □(A → B); □A ⊢ •(A → B) \end{matrix} ; (∧ ⊢) ; □(A → B) ∧ □A ⊢ •(A → B) ; (dp) ; •(□(A → B) ∧ □A) ⊢ A → B & \begin{matrix}^{A ⊢ A (□ ⊢) □A ⊢ •A} & (M ⊢) & □(A → B); □A ⊢ •A \\ (∧ ⊢) \\ □(A → B) ∧ □A ⊢ •A \end{matrix} ; (dp) ; •(□(A → B) ∧ □A) ⊢ A & (⊢ ∧) & •(□(A → B) ∧ □A); •(□(A → B) ∧ □A) ⊢ (A → B) ∧ A \\ (C ⊢) \\ •(□(A → B) ∧ □A) ⊢ (A → B) ∧ A \end{matrix} ; (dp, ⊢ □) ; □(A → B) ∧ □A ⊢ □((A → B) ∧ A) ; (1)

\begin{aligned}A ⊢ A & B ⊢ B & (→⊢) & A → B ⊢ ∗A; B \\ & (⊢ P) \\ A → B ⊢ B; ∗A \end{aligned} ; (dp) ; A → B; A ⊢ B ; (∧ ⊢) ; (A → B) ∧ A ⊢ B ; (□ ⊢) ; □((A → B) ∧ A) ⊢ •B ; (2)

□(A → B) ⊢ □(A → B)  □A ⊢ □A (⊢ ∧) □(A → B); □A ⊢ □(A → B) ∧ □A  ^{(1)  (2)  (cut) □(A → B) ∧ □A ⊢ •B} (cut) □(A → B); □A ⊢ •B

(⊢ □) □(A → B); □A ⊢ □B

(⊢→) □(A → B) ⊢ □A → □B

Fig. 3. Proof of the K rule from [Wan94]

.

7 Automatic Cut-Elimination

In backwards proof search, using the cut rule involves guessing the arbitrary formula A; this is a disadvantage in automated proof, as there are infinitely many choices for A. The cut rule is the only rule with this property; in all the other rules, every formula variable appearing in a premise also appears in the conclusion. Therefore, if the cut rule can be avoided, then at each stage of a backward proof search there is only a finite number of possible next steps. However, proofs using (cut) can often be easier to construct, and (cut) is necessary to make use of previously proved lemmata.

\begin{matrix}\begin{aligned}A ⊢ A & B ⊢ B & (→⊢) & A → B ⊢ ∗A; B \\ & (⊢ P) \\ A → B ⊢ B; ∗A \end{aligned} & (□ ⊢) & □(A → B) ⊢ •(B; ∗A) \\ (M ⊢) \\ □(A → B); □A ⊢ •(B; ∗A) \end{matrix} ; (dps) ; A ⊢ ∗ • (□(A → B); □A); B ; (□ ⊢) ; □A ⊢ •(∗ • (□(A → B); □A); B) ; (1)

(1)  (M ⊢) □(A → B); □A ⊢ •(∗ • (□(A → B); □A); B)

(dps) •(□(A → B); □A); •(□(A → B); □A) ⊢ B

(C ⊢) •(□(A → B); □A) ⊢ B

(dp) □(A → B); □A ⊢ •B

(⊢ □) □(A → B); □A ⊢ □B

(⊢→) □(A → B) ⊢ □A → □B

Fig. 4. Cut-Free Proof of the K rule

The calculus δK_{t} enjoys cut-elimination because its rules satisfy the conditions (C1) to (C8) ([Bel82,Wan94]). The construction described in this section eliminates the uses of (cut) from a given δK_{t} proof, converting a proof using (cut) to one not using (cut). This demonstrates the procedure used in the proof of the cut-elimination theorem. It also allows a user to construct proofs using (cut), knowing that a cut-free proof can be obtained automatically if desired.

The cut-elimination procedure is sketched in [Gor97, Appendix]. In Fig. 4 we show the cut-free proof of the K rule obtained by our automated cut-elimination procedure. It has been abbreviated by combining multiple display postulate steps into one step labelled “(dps)”. Also, the automated procedure sometimes produces steps whose premise and conclusion are the same, or a step followed by its inverse. These have been omitted. It will be noted that, apart from the display postulate steps, all the other steps used also appear in the proof in Fig. 3, but many of the introduction rule steps in that proof do not appear in the cut-free proof. However, it is known that in general, the cut-free proof can be exponentially longer than the proof from which it is constructed.

8 Further Work and Conclusions

The work described here could be extended to multi-modal logics. In δK_{t}, the structural connective • is a proxy for the logical connectives ♦ and □. The structural construction ∗•∗ is a proxy for the logical connectives ◇ and ■, since ∗ is a proxy for Boolean negation ¬. As noted in §6, further primitive axioms can be added to δK_{t} as structural rules to obtain numerous modal extensions.

To cater for multiple modalities like ◇_{i}, ♦_{i}, □_{i}, ■_{i}, 1 ≤ i ≤ n, we simply invent n structural proxies •_{i}, 1 ≤ i ≤ n. Adding appropriate structural rules then allows you to build a hybrid multi-modal logic of your choice. Furthermore, if the interaction axioms for these modalities are primitive [Kra96], you can add these interactions as structural rules. Cut-elimination then comes for free.

Cut-free display calculi do not enjoy the substructure property, although they do enjoy the subformula property. Therefore our rules do not immediately give a decision procedure. Since many tense logics are decidable, further work is required to control automatic proof search using display calculi.

References

[AB75] A R Anderson and N D Belnap. Entailment: The Logic of Relevance and Necessity, 1. Princeton University Press, Princeton, USA, 1975.

[Bel82] N D Belnap. Display logic. J. of Philosophical Logic, 11:375–417, 1982.

[BGH95] J Barwise, D Gabbay, and C Hartonas. On the logic of information flow. Bulletin of the IGPL, 3(1):7–49, 1995.

[Cer82] L Farinas Del Cerro. A simple deduction method for modal logic. Information Processing Letters, 14(2):49–51, 1982.

[Daw97] J E Dawson. Simulating term-rewriting in LPF and in display logic. (submitted), Automated Reasoning Project, 1997.

[DEL90] F Debart, P Enjalbert, and M Lescot. Multi-modal logic programming using r=equational and order-sorted logic. Technical Report 90-3, 1990.

[DG97] J E Dawson and R Goré. A mechanised proof system for relation algebra using display logic. (submitted), Automated Reasoning Project, 1997.

[DG98] S Demri and R Goré. Cut-free display calculi for nominal tense logics. (submitted), Automated Reasoning Project, 1998.

[DSH93] K Došen and P Schroeder-Heister, editors. Substructural Logics. Studies in Logic and Computation. Oxford University Press, 1993.

[FHMV95] R Fagin, J Halpern, Y Moses, and M Vardi. Reasoning about Knowledge. The MIT Press, 1995.

[Gir87] J-Y Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[Gor97] R Goré. Cut-free display calculi for relation algebras. In D van Dalen and M Bezem, editors, CSL96, LNCS 1258, 198–210. Springer, 1997.

[Gor98] R Goré. Substructural logics on display. Logic Journal of the IGPL, 6(3):451–504, 1998.

[HC96] G E Hughes and M J Cresswell. A New Introduction To Modal Logic. Routledge, 1996.

[HSZ96] A Heuerding, M Seyfried, and H Zimmermann. Efficient loop-check for backward proof search in some non-classical logics. In Tableaux 96, LNAI 1071, 210–225. Springer, 1996.

[Kra96] M Kracht. Power and weakness of the modal display calculus. In H Wansing, editor, Proof Theory of Modal Logics, 92–121. Kluwer, 1996.

[MFD96] M Wooldridge M Fisher and C Dixon. A resolution-based proof method for temporal logics of knowledge and belief. In D Gabbay and J-J Ohlbach, editors, Proceedings of FAPR’96, 178–192. Springer-Verlag, 1996.

[Ohl88] H-J Ohlbach. A resolution calculus for modal logics. In CADE-9, LNCS 310, 500–516. Springer-Verlag, 1988.

[Pau90] L C Paulson. Isabelle: The next 700 theorem provers. In P Odifreddi, editor, Logic and Computer Science, 361–385. Academic Press, 1990.

[Pra91] V Pratt. Action logic and pure induction. In JELIA90, LNCS 478, 97–120. Springer-Verlag, 1991.

[Res98] G Restall. Displaying and deciding substructural logics I: logics with contraposition. Journal of Philosophical Logic, to appear, 1998.

[Wal89] L A Wallen. Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics. MIT Press, 1989.

[Wan94] H Wansing. Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, 4:125–142, 1994.