key: cord-0046577-m66dk8i6 authors: Girlando, Marianna; Straßburger, Lutz title: MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description) date: 2020-06-06 journal: Automated Reasoning DOI: 10.1007/978-3-030-51054-1_25 sha: 1f2ecf56f75508704aa31cbbd51a04197e90e749 doc_id: 46577 cord_uid: m66dk8i6 We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion systems (Gentzen-style) and multi-conclusion systems (Maehara-style) for all logics in the intuitionistic modal IS5-cube. While the single-conclusion system are better investigated and have an internal cut-elimination, the multi-conclusion systems can provide a countermodel in case the proof search fails. To our knowledge this is the first automated theorem prover for intuitionistic modal logics. For wider usability, we also implemented classical normal modal logics in the S5-cube. In the last decade, nested sequent calculi have been successfully used to define cut-free deductive systems for various normal modal logics (classical [3] , intuitionistic [17, 23] , constructive [1] and tense logics [10] ) and non-normal modal logics [14] . For some variants there also exist focused calculi [5, 6] . Even though many of these calculi yield terminating decision procedures, most of them have not (yet) been implemented in automated theorem provers. In fact, the only implementations of nested sequent systems that we are aware of are for non-normal logics [13, 14] and normal conditional logics [18] . But for the more widely used classical and intuitionistic normal modal logics in the S5-cube no implementations using nested sequents exist. In fact, for intuitionistic modal logics we are not aware of any automated theorem provers. For this reason we present here a modular Prolog implementation for nested sequent calculi for all intuitionistic normal modal logics in the IS5-cube (see Fig. 1 ). For the systems whose decidability is known, our prover terminates. For IS4, IK4, and ID4, for which decidability is still an open problem, we cannot ensure termination. For the sake of higher usability, we included in the implementation also all classical normal modal logics in the S5-cube, but they are not discussed here, as their implementation is rather straightforward [3] . The prover, called Moin 1 (for MOdal Intuitionistic Nested sequents), is inspired by the lean deduction methodology introduced in [2] : the program is constituted by a set of Prolog clauses, one for each inference rule of the calculus, and the proof search is provided by the Prolog depth-first mechanism 2 . The advantages of this approach, as stated in [2] , are high degree of adaptability and safety (i.e. the Prolog clauses are easy to verify), and high efficiency. This article is organized as follows. Section 2 introduces intuitionistic modal logics; Sect. 3 and 4 present nested sequents (single-and multi-conclusion) and the proof systems we use. Section 5 treats termination and countermodel construction, and Sect. 6 describes the main features of Moin. We consider here the variant of intuitionistic modal logic that has first been studied in [7] and [20] , and then been investigated in detail by Simpson in his PhD-thesis [22] . It is obtained from intuitionistic propositional logic, by adding the two modalities and ♦, together with the necessitation rule (if A is provable, then so is A), and the following five axioms: In classical modal logic, only k 1 is added, as the others follow via the De Morgan duality between and ♦, which is not present in the intuitionistic case. But as in the classical case, we can extend the logic by additional axioms. We restrict ourselves here to the five axioms d, t, b, 4 and 5, which in the classical as well as in the intuitionistic case generate 15 different logics, which can be arranged in the so-called S5-cube (classical) or IS5-cube (intuitionistic). Figure 1 shows the intuitionistic variant of that cube, together with the five aforementioned axioms. The reason for the restriction to these logics in this presentation is that the nested sequent proof systems for them are particularly well-studied [3, 5, 6, 8, 17, 23] . The Prolog code is written in a way that it can easily be extended to other logics. The semantics of the logics in the IS5-cube is defined in terms of bi-relational models, introduced in [7, 20, 22] . No complexity results are known for these logics; however, their complexity has to be at least PSPACE-hard, as intuitionistic propositional logic is PSPACE-complete. Nested sequents have been introduced independently in [3, 11] , and [21] . Whereas an ordinary sequent is a list (or multiset or set) of formulas, a nested sequent is where A 1 , . . . , A n are formulas and Γ 1 , . . . , Γ m are nested sequents. This corresponds to a one-sided setting, and the formula interpretation fm(Γ ) of the sequent above isfm( This setting is used by Brünnler in [3] , to give cut-free systems for all logics in the classical S5-cube, including a decision procedure. He has also shown how a finite countermodel can be extracted from a failed proof search. We implemented his method in Moin, but we will not go into details here because there are already many different provers for classical modal logic in the literature 3 , and the details of our implementation for classical modal logics follow straightforwardly from our implementation for intuitionistic modal logics, that we discuss below. The first observation is that for intuitionistic logic we need two-sided sequents, which are formally generated by where A 1 , . . . , A n are the formulas that would occur on the left of the turnstile if there was a turnstile, B 1 , . . . , B k are the formulas that would occur on the right of the turnstile if there was a turnstile, and Γ 1 , . . . , Γ m are nested sequents. We use the •and •-superscripts as polarity indication for formulas. In this (multi-conclusion) intuitionistic two-sided setting, it is not possible to give a formula interpretation as in the one-side classical case. However, this is possible in the single-conclusion setting, where there is only one formula B • in the whole sequent. Single-conclusion sequents are formally generated by where Γ stands for a (non-empty) sequent that contains exactly one formula with •-polarity, and Λ for a (possibly empty) sequent in which all formulas have •-polarity. Then the formula interpretation is: In order to define inference rules on nested sequents, we need the notion of context, denoted as Γ {·}, which is a nested sequent that contains exactly one occurrence of the hole {·} in the place of a formula (of either polarity). There are two kinds of nested sequent systems for intuitionistic logic: singleconclusion [6, 17, 23] in the style of Gentzen [9] and multi-conclusion [12] , in the style of Maehara [15] . In Moin, we implemented both. More precisely, we implemented the single-conclusion systems of [23] and (a minor variation of) the multi-conclusion systems presented in [12] . Figure 2 shows the basic single-conclusion system NIKs for the modal logic IK as presented in [23] . Formulas marked in gray are formally not part of the rules, but are part of the implementation in order to ease termination checks, and to reduce the search space. Gray formulas can never be principal in a rule application; they are kept in the premisses for book-keeping. The use of Γ * in the ⊃ • s -rule is due to the fact that every sequent occurring in a proof has to be a single-conclusion sequent. Then, Fig. 3 shows the extension rules corresponding to the axioms in Fig. 1 . They are taken from [23] , and we refer the reader to [23] or [17] for a discussion on which set of rules gives which logic in the cube in Fig. 1 . For a set X ⊆ {d, t, b, 4, 5}, we write NIKs + X for the system obtained from NIKs by adding the corresponding rules in Fig. 3 . If d ∈ X we need in some cases also the d [] s -rule shown in Fig. 4 (see [16] for more details). 4 Finally, Fig. 4 shows the rules needed for the multi-conclusion system. For each X ⊆ {d, t, b, 4, 5}, we write NIKm + X for the system obtained from NIKs + X by removing the rules with an s in the subscript and replacing them with the s is in the system, the rules d s -rule is never needed in the multi-conclusion system. For more details see [12] . All the classical modal logics in the S5-cube are decidable, and a simple loop check in the rules that create a new nesting is enough to ensure termination (see [3] for details). It is also explained in [3] how to obtain a finite countermodel from a failed proof search, and we implemented that method in Moin. In the intuitionistic case, not all logics in the IS5-cube are known to be decidable. For the logics ID4, IK4 and IS4, this is still an open problem. But, as already observed in [22] , all other logics are decidable. Termination for logics that do not need the 4and 5-axioms can be proved similarly as in the case of propositional intuitionistic logic: the only loop-check to be performed concerns application of the ⊃ • s -rule, where it is needed to check whether the current sequent already occurs in the derivation branch. For the logics containing the 5-axiom, it is enough to restrict the depth of a sequent to 1: when the ♦ • -, • -, or one of the d-rules creates a new nesting at a depth > 1, the nesting is introduced at the root level of the sequent. Completeness of the resulting proof system has been proved in [8] . Thus, the restriction on the ⊃ • s rule mentioned above is the only loop-check needed for these systems. For the remaining logics (ID4, IK4, IS4), decidability is not known, and we implement only two naive loop-checks: one for ⊃ • s mentioned above, and one that is similar to the loop-check for classical modal logics. Refer to [22] for an explanation on why this strategy does not suffice to ensure termination. When using the single-conclusion systems, termination and completeness can easily be shown via cut-elimination [23] . However, it is not clear how to obtain a finite countermodel from a failed proof search. The reason is that there is not such a close correspondence between models and sequents as for classical modal logic. For this reason we also implemented the multi-conclusion systems of [12] . They are related to the intuitionistic (bi-relational) Kripke models [7, 20] , as classical nested sequent systems to classical Kripke models. The treestructure of the sequent tree corresponds to the R-relation (the accessibility relation for the modalities), and the tree-structure of the proof tree corresponds to the intuitionistic ≤-relation (often interpreted as future-relation). We follow the construction of [12] for obtaining a countermodel from a failed proof search, with certain simplifications, as in our case the model is always finite. Termination for NIKm + X is ensured by the same arguments as for NIKs + X, with the difference that the loop-check (which is performed for ⊃ • s in NIKs) is performed for ⊃ • m and • m in NIKm + X. Moin implements the nested sequents for classical modal logics from [3] , and the single-and multi-conclusion calculi for intuitionistic modal logics shown in s -rule, and the rules for the multi-conclusion system NIKm + X Figs. 2, 3, 4. The prover is composed of a set clauses, each implementing a rule of the sequent calculus. The structure of Moin reflects the modularity of the calculi: implementations of stronger systems are obtained by adding the clauses corresponding to the rules to the set of clauses for weaker systems. The biggest difficulty in implementing nested sequents lies in the choice of the data structure. For ordinary sequents, it is straightforward to use the Prologlists. However, nested sequents are not lists of formulas, but trees of lists of formulas, and Prolog does not come with an efficient representation of trees, which would allow formulas occurring in lists inside a node of the tree to be easily accessed and replaced. There exist several approaches to overcome this difficulty. The implementation of conditional modal logics in [18] and of non-normal modal logics in [14] implement nested sequents as nested lists, while the implementation of non-normal modal logics in [13] uses a tree structure, in which nodes are annotated with sequents. We follow a different approach, representing nested sequents as Prolog lists with annotations. This can be compared to labelled calculi [22] : an annotation is an index labelling formulas of a nested sequent, with formulas occurring at the same node sharing the same annotation. This data structure allows for an easier countermodel extraction from a failed branch. Propositional variables are represented in Moin as Prolog atoms a,b,. . . ; ⊥ and are Prolog false and true, and the connectives ¬, ∧, ∨, ⊃, and ♦ are respectively represented by~, v^, ->, ! and ?. Nested sequents for classical modal logic are represented by means of two Prolog lists Rel,Seq. Seq is a list of triples (X,F,Sign), where F is a formula in Moin syntax, X is the annotation of F, i.e., an integer keeping track of the component of the nested sequent at which the formula occurs, and Sign is either + or -. Rules can only be applied to formulas with a positive sign, while formulas with a negative sign are used for book-keeping (they are the gray formulas from Figs. 2, 3 and 4). Rel is a list of pairs (X,Y), representing the parent-child relation between nodes of a nested sequent. Single-conclusion nested sequents are represented as Rel,Lambda,Out, where Lambda is a list of elements (X,F,Sign) storing the •-formulas, and Out is a pair (X,F) storing the •-formula. Finally, multi-conclusion nested sequents are represented by means of three lists Rel,Gamma,Delta, where Gamma and Delta are lists of elements (X,F,Sign), respectively representing •and •-formulas. Proof search is invoked by the predicate derive(PS,Axioms,F), where F is the formula to be checked, PS selects the proof system (k for classical, i for intuitionistic single-conclusion, m for intuitionistic multi-conclusion nested sequents), and Axioms is a (possibly empty) list specifying the additional axioms to be used (d, t, b, 4 and 5). For instance, derive(i, [b,5] , (?a -> !?a)^(?!a -> !a)) triggers the derivation of axiom 5 in NIKs + {b, 5}. The predicate derive queries the corresponding predicate prove_k\4, prove_i\3 or prove_m\4. These predicates are recursively invoked and generate the proof-search tree (and the countermodel). To ensure termination, application of some rules needs to be restricted (see Sect. 5). The loop-checks are implemented by auxiliary predicates. The application of prove to a branch stops when an axiom clause is reached (success), or when no clause succeeds, producing a A = 1, . . . , 8(a ⊃ b) ⊃ ( 1, . . . , 8 a ⊃ 1, . . . , 8 b) B = (♦1, . . . , ♦5a ⊃ 1, . . . , 5b) ⊃ 1, . . . , 5(a 5 . Formulas A and B are generated by adding modal operators to k1 and k4, and are both derivable in all systems. Formulas C and D are from [4] ; C is valid in all systems with 4 and D in all systems with b. Formula E is not derivable in any system. ID IT IKB IK5 IK45 IKB5 IDB ID5 ID45 ITB IS5 A 0, 1 · 0, 1 0, 1 · 0, 7 0, 2 · 0, 2 0, 1 · 0, 1 19, 6 · 0, 2 113, 9 · 0, 3 16, 1 · 0, 3 0, 2 · 38, 7 * · * * · * 0, 2 · 0, 2 32, 8 · 0, 5 B 0, 1 · 0, 1 0, 1 · 0, 2 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 2 0, 1 · 0, 2 0, 1 · 0, 5 0, 2 · 40, 2 0, 2 · 46, 2 0, 1 · 0, 1 0, 1 · 0, 2 C 0, 1 · 0, 1 0, 3 · 0, 1 0, 1 · 0, 1 0, 6 · 0, 1 0, 2 · 0, 1 0, 1 · 0, 1 0, 2 · 0, 1 3, 0 · 0, 1 8, 1 · 0, 1 0, 1 · 0, 1 1, 2 · 0, 1 0, 1 · 0, 1 D 0, 1 · 0, 2 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 E 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 1 0, 1 · 0, 3 0, 1 · 0, 8 0, 1 · 0, 1 0, 1 · 0, 1 failed branch. In case of success of the proof-search, Moin produces a file containing the derivation. Otherwise, for classical and intuitionistic multiconclusion sequents, Moin prints out a countermodel in a file. While in the classical system the information contained in the leaf of a failed branch is enough to extract a countermodel, this is not the case for NIKm + X, where all the failed branches need to be considered. Due to the absence of benchmarks for intuitionistic modal logics, we have measured the performance Moin with some adhoc (valid and non valid) formulas shown in Fig. 5 . The construction of a set of benchmark formulas has to be postponed to future work, as the 15 different logics in the IS5-cube make this not an easy task. We used SWI Prolog 8.0.3 on a Dell XPS 13 9370 laptop running with a 1.80 GHz Quad Core, Intel Core i7-8550U, 8 GB RAM, under Linux Mint 19.1. The numbers reported in the Fig. 6 are the results given in seconds of the user time command from bash script, approximated at 0,05 s. Numbers in red (left side) are the results of the single-conclusion calculus, numbers in blue (right side) of the multi-conclusion one. We removed the -output part from Moin before proceeding to the tests. The results vary depending on the formula under scope. In some cases (formula A tested in IK45 and IS5; formula C in IDB, ID5) the implementation of NIKm + X seems to have better performances than the one of NIKs + X, since the multi-conclusion prover has a smaller number of backtrack points (only the rules ⊃ • m and • m are non-invertible). In some other cases (formula A tested in IDB; formula B tested in ID5 and ID45), the NIKm + X prover is slower than the NIKs + X one: this is due to the fact that in the multi-conclusion implementation the order in which the rules are applied is different from the single-conclusion one, and a larger number of sequents can be introduced in the proof search. On nested sequents for constructive modal logics leanTAP: lean tableau-based deduction Deep sequent systems for modal logic TABLEAUX: a general theorem prover for modal logics Focused and synthetic nested sequents Modular focused proof systems for intuitionistic modal logics 18. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik Axiomatizations for some intuitionistic modal logics Label-free proof systems for intuitionistic modal logic IS5 Untersuchungenüber das logische Schließen Cut-elimination and proof search for biintuitionistic tense logic Cut-free sequent calculi for some tense logics Maehara-style modal nested calculi Combining monotone and normal modal logic in nested sequentswith countermodels Modularisation of sequent calculi for normal and nonnormal modalities Eine darstellung der intuitionistischen logik in der klassischen Modal proof theory through a focused telescope Label-free modular systems for classical and intuitionistic modal logics NESCOND: an implementation of nested sequent calculi for conditional logics How to build an automated theorem prover A framework for intuitionistic modal logic The method of tree-hypersequents for modal propositional logic The proof theory and semantics of intuitionistic modal logic Cut elimination in nested sequents for intuitionistic modal logics The main purpose of Moin is to be a tool for experimentation. The proof theory of intuitionistic modal logics has seen many advances in the last decade, and we felt the need for a tool that makes these advances accessible to a wider audience. We also hope to get through the use of Moin some new insights in the decision problem for ID4, IK4 and IS4.Further future work is to find more efficient implementations of the termination checks and to implement the focused systems of [5, 6] .