On interactive proof-search for constructive modal necessity Favio E. Miranda-Perea, Lourdes del Carmen González Huesca, and P. Selene Linares-Arévalo Departamento de Matemáticas, Facultad de Ciencias, Universidad Nacional Autónoma de México {favio,luglzhuesca,selene linares}@ciencias.unam.mx Abstract. We present a dual sequent calculus for the necessity fragment of the constructive modal logic S4 and show its adequacy for proof-search in the style of modern interactive theorem provers. The main feature of dual systems is the use of two contexts to capture the notions of true and valid formulas, without using any formal semantics. This attribute allows us to give simple rules for the  operator that, most of the time, grant the substitution of a strict modal reasoning by a pure propositional one, thus simplifying the proof-search process. Moreover, we introduce a formal notion of backward proof corresponding to a bottom-up construction of a derivation tree by means of a left-to-right depth-first proof-search. Keywords: Constructive Modal logic · Proof-search · necessity · sequent calculus 1 Introduction Modal logics play an important role in several areas of Computer Science and Philosophy. For instance, various type systems for concurrent and distributed computations [12,15] employ modalities and a modal lambda calculus has been proposed to model information flow in computer networks[4]. In Artificial Intelli- gence (AI) they are useful to model knowledge structures among agents, ontolo- gies or the behaviour of computer systems. These and other applications oblige to design effective and simple to use procedures for proof search in modal logics. However, the existing processes are quite sophisticated, for instance [17,1], and machine-oriented in the sense that their inference rules deviate from the natural human reasoning, for they are or intend to be fully automated, like the bidirec- tional approach of [10]. This makes the modelling of actual arguments involving modal reasoning difficult. Such arguments arise for instance in AI, while veri- fying an agent-based computer system; or in Philosophy, in the representation of concrete cases in modal argumentation theory, where the  operator usually represents the argument attack relation [3,8]. In this paper we walk in the opposite direction by proposing a sequent cal- culus adequate for proof-search but in an interactive style, as is understood and Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0) 106 implemented in modern proof-assistants like Coq. This means that the proof- search is driven by the human agent: the process starts with the desired sequent S; if it is suitable as a conclusion of some rule, then the process continues with the premises of this rule. If at the end all branches of this search end in an axiom or initial rule, the procedure is succesful. The purpose of this work is to give a precise formal definition of this process and to prove its equivalence with the usual forward proof construction in the case of constructive modal logic S4 for necessity. 2 A Dual Sequent Calculus for Necessity The formal system GS4 hereby considered is a sequent calculus whose foun- dations come from the analysis of [13]. Propositions are analysed judgmentally without any semantic label (worlds). In the specific case of modal connectives by means of judgments over propositions. The notion of so-called hypothetical judg- ments is extended to categorical judgment where a conclusion does not depend on hypotheses about the constructive truth of propositions. Hence, a distinction of two forms of primitive judgments is essential: ‘A true’ means that we know how to verify A under hypothetical judgments, whereas ‘A valid ’ represents the fact that A is a proposition whose truth does not depend on any hypotheses, thus internalizing a categorical judgment as a proposition syntactically represented by the modal formula A. The system is called dual for it handles sequents with two separate contexts of the form ∆|Γ ` A. We chose to implement such contexts by means of two disjoint lists (instead of sets or multisets), ∆ for valid and Γ for true hypotheses. This choice allows us to omit the labels valid, true in context formulae, contrary to [16]. A similar separation is present in several works: for instance the systems of [6] use global and local assumptions or the work of [2] which discusses modal logic encodings by using separate consequence relations (semantical and deductive) related to classical validity and truth. The idea behind the context separation in GS4 is that formulae in ∆ are modal (i.e. boxed formulae), whereas those in Γ are propositional. Nevertheless, like the intuitive semantic qualifiers, this idea does not represent a syntactic restriction, we can have arbitrary formulae in both contexts. Moreover, the succedent of a sequent only considers true propositions, there is no need to consider valid con- clusions explicitly as they are represented by the formula A. For the sake of self-containment let us briefly review the elements of our syntax. Modal formulae are generated by the following grammar: A, B ::= pn | A → B | A ∧ B | A ∨ B | A where pn denotes an element taken from an infinite supply of propositional variables, indexed by a natural number. Let us also note that we do not consider neither negation nor the constant ⊥. Therefore we will be dealing with minimal propositional logic [18] extended with the necessity operator. A particular modal logic is generated by adding suitable axioms. It is important to remark that 107 the logic here discussed is called constructive due to the approach of Martin- Löf but also to distinguish it from both, the classical modal logics where the  operator obeys the axiom A ↔ ¬♦¬A and the intuitionistic modal logics which include the axiom ¬♦⊥. In contrast, in the constructive modal logic S4 the above axioms are omitted and both modalities are primitive. Our work only considers the necessity modality . Contexts are implemented by means of so-called snoc lists: Γ, ∆ ::= · | Γ, A These are finite lists built from the empty list, denoted here by ·, and a construc- tor that generates a new list from a given one by adding a new element to its right-end. The constructor called snoc is denoted by a comma. Therefore Γ, A is the context obtained by adding A after the last element in Γ . This constructor is opposed to the traditional cons operation, predefined in functional languages, which adds elements at the left-end of the list 1 . The snoc lists provide a for- malization akin to the usual practice in computer science logic where the last context formula is the one introduced or discharged to prove an implication. The concatenation operation is inductively defined in the obvious way and denoted by Γ1 ; Γ2 . Also, whenever we write Γ, A; Γ 0 it means (Γ, A); Γ 0 , that is, the for- mula A is associated to the left context. This should be clear, for the expression Γ, (A; Γ 0 ) is ill-formed. The system GS4 is defined by the following inference rules: – Starting rules (Thyp) (Vhyp) ∆|Γ, A; Γ 0 ` A ∆, A; ∆0 |Γ ` A – Right rules ∆|Γ, A ` B ∆|Γ ` A ∆|Γ ` B (→ R) (∧ R) ∆|Γ ` A → B ∆|Γ ` A ∧ B ∆|Γ ` A ∆|Γ ` B (∨ R) (∨ R) ∆|Γ ` A ∨ B ∆|Γ ` A ∨ B ∆|· ` A ( R) ∆|Γ ` A – Left rules for truth contexts. ∆|Γ, A; Γ 0 ` C ∆|Γ, B; Γ 0 ` C ∆|Γ, A, B; Γ 0 ` C (∨ L) (∧L) ∆|Γ, A ∨ B; Γ 0 ` C ∆|Γ, A ∧ B; Γ 0 ` C ∆|Γ, A → B; Γ 0 ` A ∆, A|Γ ; Γ 0 ` B (→L) ( L) ∆|Γ, A → B; Γ 0 ` B ∆|Γ, A; Γ 0 ` B 1 The name cons is for constructor and note that snoc is the backward reading of cons. 108 – Left rules for valid contexts. ∆, A; ∆0 |Γ ` C ∆, B; ∆0 |Γ ` C ∆, A, B; ∆0 |Γ ` C (∨ LV) (∧LV) ∆, A ∨ B; ∆0 |Γ ` C ∆, A ∧ B; ∆0 |Γ ` C ∆, A → B; ∆0 |Γ ` A ∆, A; ∆0 |Γ ` B (→LV) ( LV) ∆, A → B; ∆0 |Γ ` B ∆, A; ∆0 |Γ ` B – Cut rules ∆|Γ ` A ∆|Γ, A ` B ∆|· ` A ∆, A|Γ ` B (Cut) (CutV) ∆|Γ ` B ∆|Γ ` B We have two starting rules allowing to use an hypothesis present in any of the two contexts; the right rules for the connectives are the usual ones; the left rules come in two versions, one for each context. For the case of conjunction and disjunction these rules are also usual. The left rules for implication are new2 , to the best of our knowledge and capture the direct use of an implication to prove its consequent. The right rule for  corresponds to the necessitation rule. Observe that we can introduce a formula A only in the case when we derive A without resorting to any true hypothesis. This formulation is the key to validate the deduction theorem in Hilbert axiomatic systems for modal logic. See for instance [9]. The left rule L is discussed in our previous work [5] and represents a transference principle between contexts: we can move a valid hypothesis A to the truth context by modalizing it. Finally LV says that to use an assumption A which is valid, it suffices to use only A. These left rules for necessity allow to replace a modal reasoning about A, for a propositional reasoning about A. Let us show a couple of derivations in our system. Example 1. The following is a proof of  ·|· ` (A → B) →  A → (C → B) (1) A → B , A|· ` A Vhyp (2) A → B , A|C ` A  R (1) (3) A → B , A|C ` B → L (2) (4) A → B , A|· ` C → B → R (3) (5) A → B , A|· ` (C → B)  R (4) (6) A → B|A ` (C → B)  L (5) (7) A → B|· ` A → (C → B)  → R (6) (8) A → B|· `  A → (C → B)   R (7) (9) ·|(A → B) `  A → (C → B)   L (8) (10) ·|· ` (A → B) →  A → (C → B) → R (9) 2 Except for a mention in our previous work [14] 109 Example 2. The following is a proof of    (B → A) ∧ (C → A) |· `  B ∨ C → A (1) B → A , C → A|B ` B Thyp (2) B → A , C → A|B ` A → LV (1) (3) B → A , C → A|C ` C Thyp (4) B → A , C → A|C ` A → LV (3) (5) B → A , C → A|B ∨ C ` A ∨ L (2, 4) (6) B → A , C → A|· ` B ∨ C → A → R (5) (7) B → A , C → A|· ` (B ∨ C → A)  R (6) (8) (B → A) ∧ (C → A)|· ` (B ∨ C → A) ∧ L (7) (9) ((B → A) ∧ (C → A))|· ` (B ∨ C → A)  LV (8) The above proofs can be read according to the usual definition of forward derivation, though actually they were gained from a bottom-up proof construc- tion process, which corresponds to the below notion of derivation given originally by Kanger [11]. Definition 1 (Derivation à la Kanger). A proof or derivation of ∆|Γ ` A is a finite sequence of sequents Π = hJ1 , . . . , Jk i such that J1 is ∆|Γ ` A and for every 1 ≤ i ≤ k one of the following conditions hold: – Ji is an instance of the (Hyp) or (VHyp) rules. – For every 1 ≤ i ≤ k, Ji is the conclusion of an instance of some inference rule with premise Jj with j > i, or premises Jj , Jl with j, l > i. Thus, a derivation starts with the sequent sought after, whereas the usual notion of formal proof ends with it. Also, for any given sequent, the premisses that allow to conclude it appear later in the sequence. This gives an idea of backward proof. Regrettably, even when this intuitive notion permeates Kanger’s work, the concept is not engaged, for the proofs there are written forwards. Moreover, like the examples above show, the mere sequence does not let us keep a trace of the proof-search process. Our purpose here is to give a formal notion of backward proof for modal logic that corresponds to the kind of techniques implemented in proof assistants, thus resolving the just mentioned issues. But first let us observe that GS4 indeed captures the constructive modal logic S4 for necessity. Theorem 1. The sequent calculus GS4 exactly captures the constructive modal logic S4 Proof (Sketch). It is easy to show that the characteristic axioms of S4, namely K, T and 4 are derivable in GS4. Moreover, by structural induction on the re- spective derivability relations, we can show that GS4 is equivalent to the dual natural deduction system NS4 of [5] (we omit the proof details due to lack of space), where we also give a detailed and formally verified proof of the equiva- lence of NS4 with an axiomatic system for S4. 110 3 Backward proofs in GS4 To being able to formalize our notion of backward proof, let us first introduce a useful device to sequents, namely labelled hypotheses [7], which are pairs of the form H : A where H is a label or shortcut to refer to A. The set of labels is taken to be disjoint with the set of names in the current signature. A labelled context Γ is a set of labelled hypotheses Γ = {H1 : A1 , . . . , Hn : An } where Hi 6= Hj , if i 6= j. Moreover, in a context of the form Γ, H : A; Γ 0 we assume that A is not in Γ ; Γ 0 and that H is a new label not used in Γ ; Γ 0 . The use of labels does not contribute much to the usual system of forward derivations, but as we will see soon it is very useful to the backward approach. In the following we use labelled contexts where they account for simplicity. Otherwise, we use conventional contexts. The process of backward proof construction of a given sequent S consists of searching for an inference rule R whose conclusion matches S and then to continue the proof-search with the premisses S or S1 , S2 of R. This backward reading of the inference rules is called a tactic. A backward proof will be a particular sequence of tactics. Let us formalise these concepts. Definition 2. A goal G is any sequent ∆|Γ ` A. The set of finite sequences of goals GSeq is recursively defined as follows: S ::= [·] | (G :: S) where [·] denotes the empty goal sequence. Moreover, if S1 , S2 ∈ GSeq then by S1 ; S2 we mean the concatenation3 of S1 with S2 . We define now a transition system of tactics corresponding to backward proof-search. Definition 3. The transition system of tactics for GS4 is defined as follows: – The non-empty set of states is the set of goal sequences GSeq. – An initial state is a singleton sequence4 . – [·] is the unique terminal state. – The transition relation B ⊆ GSeq × GSeq is inductively defined by the below axioms and inference rule, where a transition S1 B S2 can be read as “to prove the sequents in S1 it suffices to prove the sequents in S2 ”. Conclusion analysis (right sequent rules): • intro H: ∆|Γ ` A → B B ∆|Γ, H : A ` B • split: ∆|Γ ` A ∧ B B ∆|Γ ` A; ∆|Γ ` B • left: ∆|Γ ` A ∨ B B ∆|Γ ` A • right: ∆|Γ ` A ∨ B B ∆|Γ ` B 3 We use the ; for concatenation in both cases: contexts and goal sequences. 4 For clarity, a singleton sequence is identified with its unique element. That is, we write ∆|Γ ` A instead of (∆|Γ ` A :: [·]) 111 • necessitation: ∆|Γ ` A B ∆|· ` A Premise analysis (left sequent rules): • apply H: ∆|Γ, H : A → B; Γ 0 ` B B ∆|Γ, H : A → B; Γ 0 ` A • apply H: ∆, H : A → B; ∆0 |Γ ` B B ∆, H : A → B; ∆0 |Γ ` A • destruct H:∆|Γ, H : A ∧ B; Γ 0 ` C B ∆|Γ, H1 : A, H2 : B; Γ 0 ` C • destruct H:∆, H : A ∧ B; ∆0 |Γ ` C B ∆, H1 : A, H2 : B; ∆0 |Γ ` C • destruct H: ∆|Γ, H : A ∨ B; Γ 0 ` C B ∆|Γ, H1 : A; Γ 0 ` C ; ∆|Γ, H2 : B; Γ 0 ` C • destruct H: ∆, H : A ∨ B; ∆ |Γ ` C B ∆, H1 : A; ∆0 |Γ ` C ; 0 ∆, H2 : B; ∆0 |Γ ` C • destruct H: ∆|Γ, H : A; Γ ` B B ∆, H1 : A|Γ ; Γ 0 ` B 0 • destruct H: ∆, H : A; ∆0 |Γ ` B B ∆, H : A; ∆0 |Γ ` B Lemma Assertion: • assert A: ∆|Γ ` C B ∆|Γ ` A; ∆|Γ, H : A ` C • cut A: ∆|Γ ` C B ∆|Γ, H : A ` C; ∆|Γ ` A • vassert A: ∆|Γ ` C B ∆|· ` A; ∆, H : A|Γ ` C • vcut A: ∆|Γ ` C B ∆, H : A|Γ ` C ; ∆|· ` A Discarding tactics: • assumption: ∆|Γ, A; Γ 0 ` A B [·]. • vassumption: ∆, A; ∆0 |Γ ` A B [·]. Sequencing: S1 B S2 (seq) S1 ; S B S2 ; S A basic transition transforms a singleton goal sequence into a, perhaps empty, sequence of subgoals dictated by the backwards reading of an inference rule of GS4. The (seq) rule determines the order in which goals are solved, namely from the first (most left) goal in the current sequence of pending goals. Also observe that each cut rule has two corresponding tactics, namely cut and assert. The difference being only operational: either we first prove the lemma and then use it or viceversa. Finally we can give the promised definition of a backward proof. Definition 4. A backward proof of ∆|Γ ` A is a finite sequence of states S1 , . . . , Sk such that – S1 is ∆|Γ ` A – For every 1 ≤ i < k, Si B Si+1 – Sk is [·] Therefore a backward proof of a sequent ∆|Γ ` A is a finite sequence of tactics that ends in the empty sequence of goals [·], meaning that the proof-search of the original goal ∆|Γ ` A has no pending subgoals left to prove. This transition sequence of tactics corresponds to the bottom-up construction of a derivation tree by means of a left-to-right depth-first proof search. Let us present now some particular examples of backward proofs that intend to show the adequacy of our secuent calculus GS4 for interactive proof-search. 112 Example 3. The following is a backward proof of    ·|H1 :  (P → Q) ∨ R `  (P ∨ R) → (Q ∨ R)    ·|H1 :  (P → Q) ∨ R `  (P ∨ R) → (Q ∨ R) B   destruct H1 H1 : (P → Q) ∨ R|· `  (P ∨ R) → (Q ∨ R) B necessitation H1 : (P → Q) ∨ R|· ` (P ∨ R) → (Q ∨ R) B intro H2 H1 : (P → Q) ∨ R|H2 : (P ∨ R) ` (Q ∨ R) B destruct H2 H1 : (P → Q) ∨ R , H2 : P ∨ R|· ` (Q ∨ R) B necessitation H1 : (P → Q) ∨ R , H2 : P ∨ R|· ` Q ∨ R B destruct H2 H1 : (P → Q) ∨ R , H2 : P |· ` Q ∨ R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B destruct H1 H1 : P → Q , H2 : P |· ` Q ∨ R ; H1 : R , H2 : P |· ` Q ∨ R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B left H1 : P → Q , H2 : P |· ` Q ; H1 : R , H2 : P |· ` Q ∨ R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B apply H1 H1 : P → Q , H2 : P |· ` P ; H1 : R , H2 : P |· ` Q ∨ R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B vassumption H1 : R , H2 : P |· ` Q ∨ R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B right H1 : R , H2 : P |· ` R ; H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B vassumption H1 : (P → Q) ∨ R , H2 : R|· ` Q ∨ R B right H1 : (P → Q) ∨ R , H2 : R|· ` R B vassumption [·] 113 Example 4. The following is a proof of ∆|· ` (A ∧ D) → E where ∆ =def H1 : A → (B ∧ C), H2 : (D ∧ C) → (E ∧ F ). ∆|· ` (A ∧ D) → E B intro H3 ∆|H3 : (A ∧ D) ` E B destruct H3 ∆ , H3 : A ∧ D|· ` E B destruct H3 ∆ , H3 : A , H4 : D|· ` E B vassert (B ∧ C) ∆ , H3 : A , H4 : D|· ` (B ∧ C) ; ∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E B apply H1 ∆ , H3 : A , H4 : D|· ` A ; ∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E B vassumption ∆ , H3 : A , H4 : D , H5 : (B ∧ C)|· ` E B destruct H5 ∆ , H3 : A , H4 : D , H5 : B ∧ C|· ` E B destruct H5 ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` E B vassert (E ∧ F ) ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` (E ∧ F ) ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B apply H2 ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` (D ∧ C) ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B necessitation ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` D ∧ C ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B split ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` D ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` C ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B vassumption ∆ , H3 : A , H4 : D , H5 : B , H6 : C|· ` C ; ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B vassumption ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : (E ∧ F )|· ` E B destruct H7 ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : E ∧ F |· ` E B destruct H7 ∆ , H3 : A , H4 : D , H5 : B , H6 : C , H7 : E , H8 : F |· ` E B vassumption [·] 114 The above example shows the utility of the cut rule with a valid hypothesis, implemented by means of the vassert tactic. We discuss next the equivalence of backward and forward proofs. 4 Equivalence In this section we formally prove that our backward approach is equivalent to the usual notion of (forward) derivation. Let us start by noting that, according to definition 4, a backward proof is a chaining sequence of particular instances of the relation B. Therefore a backward proof of the sequent ∆|Γ ` A corresponds to an instance of the transitive closure of the B relation. For the proof of the equivalence, it will be useful to work directly with this relation. Definition 5. The transitive closure of the relation B, denoted B+ , is induc- tively defined by the following rules: S B S0 S B S 0 S 0 B+ S 00 (tc1) (tc2) S B+ S 0 S B+ S 00 Lemma 1. The following rule is admissible: S1 B+ S2 (seq + ) S1 ; S B+ S2 ; S Proof. Induction on S1 B+ S2 . If S1 B S2 , then the rule (seq) yields S1 ; S B S2 ; S and by rule (tc1) we get S1 ; S B+ S2 ; S. Assume now that S1 B S10 and S10 B+ S2 . By rule (seq) we have S1 ; S B S10 ; S and the I.H. yields S10 ; S B+ S2 ; S, therefore rule (tc2) allows us to conclude S1 ; S B+ S2 ; S. t u Definition 6. We say that a goal sequence S =def G1 , . . . , Gk is solvable, if Gi is derivable for all 1 ≤ i ≤ k. The next lemma shows that solvability of sequences is rearward preserved by the transition relation B. Lemma 2. If S1 B S2 and the sequence S2 is solvable then S1 is solvable. Proof. It is clear that the property holds for the basic transitions, since these correspond to the inference rules of our sequent calculus. The result follows by an easy induction on B. t u The above property is easily lifted to the transitive closure B+ . Lemma 3. If S1 B+ S2 and the sequence S2 is solvable then S1 is solvable. Proof. Induction on S1 B+ S2 . t u We are now ready to prove the desired equivalence. 115 Theorem 2 (Equivalence of forward and backward proofs). Let ∆|Γ ` A be any sequent. The following conditions are equivalent: – ∆|Γ ` A is derivable – ∆|Γ ` A B+ [·] Proof. The ⇐) direction is immediate from lemma 3, since the sequence [·] is trivially solvable. We prove the ⇒) direction by induction on the derivability of ∆|Γ ` A.We show here only some cases leaving the others to the reader. – Case (Vhyp). The vassumption tactic yields ∆, H : A; ∆0 |Γ ` A B [·]. – Case (∧ R). A backward derivation of ∆|Γ ` A ∧ B is the following: ∆|Γ ` A ∧ B B ∆|Γ ` A; ∆|Γ ` B B+ [·]; ∆|Γ ` B B+ [·]; [·] = [·] The split tactic yields the first transition, after that, the second step is an application of the rule (seq + ) using the IH ∆|Γ ` A B+ [·]; finally, the last step is justified by the IH ∆|Γ ` B B+ [·]. – Case (→ LV). The backward derivation of ∆, A → B; ∆0 |Γ ` B is ∆, A → B; ∆0 |Γ ` B B ∆, A → B; ∆0 |Γ ` A B+ [·] where the first step corresponds to the apply tactic and the second is given by the IH. – Case (Cut). A backward derivation of ∆|Γ ` B is given by the following transition sequence: ∆|Γ ` B B ∆|Γ ` A ; ∆|Γ, A ` B B+ [·]; ∆|Γ, A ` B B+ [·]; [·] = [·] where the first step is an instance of the assert A tactic, and the remaining are gained from the inductive hypotheses. The above theorem guarantees the reliability of the proof-search process: if ∆|Γ ` A is derivable then the interactive proof-search process succeeds and viceversa. This finishes our exposition. 5 Final Remarks In this paper we presented a dual sequent calculus GS4 for the constructive modal logic S4 of necessity, and showed that it is adequate for interactive back- ward proof-search. The rules for handling the necessity operator are simple and intuitive due to the use of dual contexts, a feature that also let us define, in a simple way, a bottom-up construction process by means of a left-to-right depth- first proof-search. This procedure was captured with a formal notion of backward proof which results equivalent to the usual definition of forward proof. This work is the first step in a study of proof-search in modal logic whose natural continu- ation consists in the proof of the cut-elimination theorem in order to validate if GS4 is loop-free and then can be also adequate for full automatization. As usual, 116 a proof of cut-elimination is not trivial. In our particular case we actually need to eliminate the two versions (Cut) and (CutV) of the cut-rule. However, the rules (L) and (LV) for the necessity operator allow us to prove the admissi- bility of (CutV) from that of (Cut) in a direct way. We are currently finding out if we can do the same for the left rules for valid contexts, a feature that would heavily simplify the proof of cut-elimination for the rule (Cut). Another part of this future inquiry is the extension of the current approach to the full modal logic S4, both constructively, where ♦ is not a dual of , but also classically. In this last case additional research about proof-search with negation is required. The final purpose of this program is to show the utility of our deductive systems for actual case studies in some specific areas, like argumentation theory in the lines of [3,8] or proof-search in multi-agent dialogues related to the work of [19]. References 1. Julius Andrikonis. Loop-free calculus for modal logic s4. i. Lithuanian Mathemat- ical Journal, 52(1):1–12, Jan 2012. 2. Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano. Encoding Modal Logics in Logical Frameworks. Studia Logica, 60(1):161–208, Jan 1998. 3. Guido Boella, Joris Hulstijn, and Leendert van der Torre. A logic of abstract argu- mentation. In Simon Parsons, Nicolas Maudet, Pavlos Moraitis, and Iyad Rahwan, editors, Argumentation in Multi-Agent Systems, pages 29–41, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. 4. Tijn Borghuis and Loe Feijs. A constructive logic for services and information flow in computer networks. The Computer Journal, 43(4):274–289, 01 2000. 5. Lourdes del Carmen Gonzlez-Huesca, Favio E. Miranda-Perea, and P. Selene Linares-Arévalo. Axiomatic and dual systems for constructive necessity, a formally verified equivalence. Journal of Applied Non-Classical Logics, 29(3):255–287, 2019. 6. Melvin C. Fitting. Proof Methods for Modal and Intuitionistic Logics. Synthese Library. Springer Netherlands, 1983. 7. D. M. Gabbay. Introduction to labelled deductive systems. In Handbook of Philo- sophical Logic, pages 179–266. Springer Netherlands, 2014. 8. Davide Grossi. Argumentation in the view of modal logic. In Peter McBurney, Iyad Rahwan, and Simon Parsons, editors, Argumentation in Multi-Agent Systems, pages 190–208, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. 9. Raul Hakli and Sara Negri. Does the deduction theorem fail for modal logic? Synthese, 187(3):849–867, 2012. 10. Samuli Heilala and Brigitte Pientka. Bidirectional decision procedures for the intuitionistic propositional modal logic is4. pages 116–131, 09 2007. 11. Stig Kanger. Provability in logic. In Ghita Holmström-Hintikka, Sten Lindström, and Rysiek Sliwinski, editors, Collected Papers of Stig Kanger with Essays on His Life and Work, volume 1 of Synthese Library: Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 8–41. Kluwer Academic Publishers (Kluwer Academic Publishers Group), 2001. Originally published as Provability in Logic. Acta Universitatis Stockholrnensis, Stockholm Studies in Philosophy I. University of Stockholm 1957. 117 12. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concur- rent linear logic programming. In Proceedings of the 7th International ACM SIG- PLAN Conference on Principles and Practice of Declarative Programming, July 11-13 2005, Lisbon, Portugal, pages 35–46, 2005. 13. Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Nordic J. Philos. Logic, 1(1):11–60, 1996. 14. Favio E. Miranda-Perea, P. Selene Linares-Arévalo, and Atocha Aliseda-Llera. How to prove it in natural deduction: A tactical approach. CoRR, abs/1507.03678, 2015. 15. Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In Proceedings of the 19th An- nual IEEE Symposium on Logic in Computer Science, LICS ’04, pages 286–295, Washington, DC, USA, 2004. IEEE Computer Society. 16. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Comp. Sci., 11(4):511–540, 2001. 17. Regimantas Pliukeviius and Aida Pliukeviien. A new method to obtain termination in backward proof search for modal logic s4. Journal of Logic and Computation, 20(1):353–379, 11 2008. 18. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Iso- morphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. 19. Martin Sticht. Proof Search in Multi-Agent Dialogues for Modal Logic. PhD thesis, University of Bamberg Press, Universitätsbibliothek Bamberg, 2018. doctoralthe- sis. 118