key: cord-0046567-apshv9tr authors: Dalmonte, Tiziano; Olivetti, Nicola; Pozzato, Gian Luca title: HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description) date: 2020-06-06 journal: Automated Reasoning DOI: 10.1007/978-3-030-51054-1_23 sha: 921aa878c798ad030d69f795139c79687c35a8d5 doc_id: 46567 cord_uid: apshv9tr We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system [Formula: see text] and its extensions with axioms M, N, and C. It is inspired by the methodology of [Image: see text], so that it does not make use of any ad-hoc control mechanism. Given a formula, HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated hypersequent. Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics. Non-Normal Modal Logics (NNMLs for short) are a generalization of ordinary modal logics that do not satisfy some axioms or rules of minimal normal modal logic K. They have been studied since the seminal works by C.I. Lewis, Scott, Lemmon, and Chellas (for an introduction see [3] ), and along the years have gained interest in several areas such as epistemic, deontic, and agent reasoning among others [1, 7, [12] [13] [14] . NNMLs are characterised by the neighbourhood semantics. In [4, 6] , a variant of it is presented, called bi-neighbourhood semantics, this variant is more suitable for logics lacking the monotonicity property, although equivalent to the standard one. Not many theorem provers for NNMLs have been developed so far. 1 In [8] optimal decision procedures are presented for the whole cube of NNMLs; these procedures reduce a validity/satisfiability checking in NNMLs to a set of SAT problems and then call an efficient SAT solver. Despite undoubtably efficient, they do not provide explicitly "proofs", nor countermodels. A theorem prover for logic EM based on a tableaux calculus very similar to the one in [10] , is presented in [9] : the system, is implemented in ELAN and handles also more complex Coalition Logic and Alternating Time Temporal logic. In [11] it is presented a Prolog implementation of a NNML containing both the [∀∀] and the [∃∀] modality; its [∃∀] fragment coincides with the logic EM, also covered by HYPNO. Finally in [5] it is presented PRONOM, a theorem prover for the whole range of NNMLs, which implements labelled sequent calculi in [6] ; PRONOM provides both proofs and countermodels in the mentioned bi-neighbourhood semantics. In this paper we describe HYPNO (HYpersequent Prover for NOn-normal modal logics) a Prolog theorem prover for the whole cube of NNMLs. The prover HYPNO implements the optimal calculi for NNMLs recently introduced in [4] . These calculi handle hypersequents, where a hypersequent represents intuitively a metalogical disjunction of sequents; sequents in themselves can be interpreted as formulas of the language. While the hypersequent structure is not strictly needed for proving formulas, it ensures a direct computation of a countermodel from one failed proof-branch. Consequently, the prover takes as input a formula and either returns a proof or a countermodel of it in the bi-neighbourhood semantics mentioned above. The Prolog implementation closely corresponds to the calculi: each rule is encoded by a Prolog clause of a prove predicate. This correspondence ensures in principle both the soundness and completeness of the theorem prover. Termination of proof search is obtained by preventing redundant application of rules. Although there are no benchmarks in the literature, the performance seems promising, in particular it outperforms the theorem prover PRONOM based on labelled calculi. The program HYPNO as well as all the Prolog source files, including those used for the performance evaluation, are available for free usage and download at http://193.51.60.97:8000/HYPNO/. We present first the axiomatization and semantics of NNMLs of the classical cube and then the hypersequent calculi implemented by HYPNO. Given a countable set of propositional variables Atm, the formulas of the language L of NNMLs are built as follows: The minimal NNML E is defined in L by extending classical propositional logic with the rule RE below. The systems of the classical cube are then obtained by adding to E any combination of axioms M, C, and N. We obtain in this way eight distinct logics (see the classical cube, below on the right), where the top system EMCN coincides with normal modal logic K. Coming to the semantics, we consider the bi-neighbourhood models [6] . As a difference with standard neighbourhood semantics, in the bi-neighbourhood one, worlds are equipped with sets of pairs of neighbours which can be thought as lower and upper approximations of neighbourhood in the standard semantics. Bi-neighbourhood models can be easily transformed into equivalent standard neighbourhood models, and vice versa. Moreover, bi-neighbourhood semantics characterises the whole cube of NNMLs [6] , in the sense that a formula A is derivable in E(M/C/N) if and only if it is valid in all bi-neighbourhood (M/N/C)models of the corresponding class. The hypersequent calculi for NNMLs implemented by HYPNO are introduced in [4] . Their syntax is as follows: a block is a structure Σ , where Σ is a multiset of formulas of L. A sequent is a pair Γ ⇒ Δ, where Γ is a multiset of formulas and blocks, and Δ is a multiset of formulas. A hypersequent is a multiset S 1 | ... | S n , where S 1 , ..., S n are sequents. Single sequents can be interpreted into the language as: The calculi implemented by HYPNO are a minor variant of the ones in [4] : they contain an additional arrow used to represent that the formulas on the left of entails the conjunction (rather than their disjunction) of the formulas on its right. By this modification, all rules of the calculi are at most binary; the equivalence of the modified calculi with the original ones in [4] is straightforward. The hypersequent calculi are defined by the rules in Fig. 1 (for propositional rules we only show the initial sequents and the rules for implication). In particular: H E := propositional rules + L + R + 1 + 2 ; H EN := H E + N; The prover HYPNO implements the calculi of Fig. 1 . It is inspired by the "lean" methodology of leanT A P [2] , even if it does not follow its style in a rigorous manner. The program comprises a set of clauses, each one of them implementing a rule or an axiom of the mentioned calculi. The proof search is provided for free by the mere depth-first search mechanism of Prolog, without any additional ad hoc mechanism. Before presenting in details the code of the theorem prover, let us discuss a general design choice. As mentioned, HYPNO searches for a derivation of an input formula and in case of failure, on demand, it produces a countermodel of it. The proof search procedure is implemented by a predicate terminating proof search which tries to generate a derivation of the given input formula. In case it fails, on demand by the user, another predicate build saturated branch is invoked that computes an open saturated branch from which a countermodel is extracted. The predicate build saturated branch is in some sense "dual" of the proof search one. We have chosen to implement a two-phase computation, instead of a single one taking care of both tasks, for the following reason: a single-phase procedure would need to carry over all information for extracting a countermodel anyway; this information would be completely useless in case of a successful derivation and would unacceptably overload proof-search. As matter of fact, the time spent to "recompute" the saturated branch is negligible with respect to the overload of a proof-search procedure storing also information for countermodel extraction. By this choice we get a simpler and more readable code, and of course, more suited for countermodel generation only "on demand". HYPNO represents an hypersequent with a Prolog list whose elements are Prolog terms of the form singleSeq([Gamma,Delta],Additional), each one representing a sequent in the hypersequent. Gamma, Delta, and Additional are in turn Prolog lists: Gamma and Delta represent the left side and the right side of the single sequent, respectively, whereas Additional keeps track of the rules already applied to each sequent in order to ensure termination by avoiding multiple redundant applications of the same rule to a given hypersequent. Elements of Gamma and Delta are either formulas or Prolog lists representing blocks. Symbols and ⊥ are represented by constants true and false, respectively, whereas connectives ¬, ∧, ∨, →, and are represented by -,^, ?, ->, and box. The symbol of provability in systems with axiom C is represented by =>. Propositional variables are represented by Prolog atoms. As an example, the Prolog list is used to represent the hypersequent (A ∧ C), , A, C ⇒ A, B, A ∨ B, B | P ⇒ P , to which the rules N, ∨ R and R have been already applied, the last one by using the block A, C and the formula B as the principal formulas. In turn, no rule has been applied to P ⇒ P (the list Additional is empty). Given a NNML formula F represented by the Prolog term f, HYPNO executes the main predicate of the prover, called prove 2 , whose only two clauses implement the functioning of HYPNO: the first clause checks whether F is valid and, in case of a failure, the second one enables the graphical interface to invoke a predicate called counter to compute a model falsifying F . In detail, the predicate prove first checks whether the formula is valid by executing the predicate: Hyper is derivable in H E . When it succeeds, the output term ProofTree matches with a representation of the derivation found by the prover. As an example, in order to prove that the sequent (A ∧ (B ∨ C)) ⇒ ((A ∧ B) ∨ (A ∧ C)) is valid in E, one queries HYPNO with the goal: Each clause of terminating proof search implements an axiom or rule of the sequent calculi H E . To search for a derivation of a sequent Γ ⇒ Δ, HYPNO proceeds as follows. First of all, if Γ ⇒ Δ is an instance of an axiom, then the goal will succeed immediately by using one of the clauses implementing the axioms. As an example, the clause implementing init is as follows: The auxiliary predicate extractPrintableSequents is used just for a graphical rendering of the hypersequent. If Γ ⇒ Δ is not an instance of the axioms, then the first applicable rule will be chosen, e.g. if Gamma contains a list Sigma representing a block Σ ∈ Γ , and Delta contains box b representing that B ∈ Δ, then the clause for R will be chosen, and HYPNO will be recursively invoked on its premises. HYPNO proceeds in a similar way for the other rules. The ordering of the clauses is such that the application of branching rules is postponed as much as possible. As an example, here is the clause implementing R : Line 3 checks whether Gamma contains an item Sigma which is a list representing a block and if a box formula box B belongs to the list Delta. Line 4 implements the restriction on the application of the rule used in order to ensure a terminating proof search: if the Additional list contains the Prolog term apdR(SigmaOrd,B) 3 , this means that the rule R has been already applied on that sequent by using B and the block Σ, and HYPNO does no longer apply it. Otherwise, the predicate terminating proof search is recursively invoked on the two premises of the rule (lines 5 and 6), by introducing Σ ⇒ B and B Σ respectively. Since the rule is invertible, Prolog cut ! is used in line 4 to eventually block backtracking. When the predicate terminating proof search fails, then the initial formula is not valid. On user demand, as recalled at the beginning of this section, HYPNO extracts a model falsifying such a formula from an open saturated branch, following the model extraction method described in [4] . The model is computed by executing the predicate: build saturated branch(Hyper, Model). When this predicate succeeds, the variable Model matches a description of an open saturated branch obtained by applying the rules of H E to the initial formula. Since the very objective of this predicate is to build an open saturated hypersequent in the sequent calculus, its clauses are essentially the same as the ones for the predicate terminating proof search, however rules introducing a branching in a backward proof search are implemented by pairs of (disjoint) clauses, each one attempting to build an open saturated hypersequent from the corresponding premise. As an example, the following clauses implement the saturation in presence of a block Σ in the left hand side and of a boxed formula B in the right hand side of a sequent: HYPNO will first try to build a countermodel by considering the left premise of R , whence recursively invoking the predicate build saturated branch on the premise with the sequent Σ ⇒ B. In case of a failure, it will carry on the saturation process by using the right premise of R with the sequent B Σ. Clauses implementing axioms for the predicate terminating proof search are replaced by the last clause, checking whether the current sequent represents an open and saturated hypersequent: build_saturated_branch(Hyper,model(Hyper)):-\+instanceOfAnAxiom(Hyper). Since this is the very last clause of build saturated branch, it is considered by HYPNO only if no other clause is applicable, then the hypersequent is saturated. The auxiliary predicate instanceOfAnAxiom checks whether the hypersequent is open by proving that it is not an instance of the axioms. The second argument matches a term model representing the countermodel extracted from Hyper. The implementation of the calculi for extensions of E is very similar: given the modularity of the calculi H E , each system is obtained by just adding clauses for both the predicates terminating proof search and build saturated branch corresponding to the specific axioms/rules. However, we provide a different Prolog file for each system of the cube. This choice is justified by two reasons: first of all readiness of the code: one may be interested only in one specific system, wishing to have all the rules in a stand-alone file. Second and more important, an implementation of calculi for a family of logic cannot be completely modular: the computation (both proof-search and countermodel extraction) is sensitive to the order of application of the rules, so that the insertion of different rules may result in different orders of application of the whole set of rules. HYPNO can be used on any computer or mobile device through a web interface implemented in php, which allows the user to choose the modal logic. When a formula is valid, HYPNO builds a pdf file showing a derivation in the corresponding calculus, as well as the L a T E X source file. Otherwise, a countermodel falsifying the initial formula is displayed. Prolog source codes are also available. We have compared the performance of HYPNO with those of the prover PRONOM [5] , which deals with the same set of logics, obtaining promising results. We have tested it by running SWI-Prolog, version 7.6.4, on an Apple MacBook Pro, 2.7 GHz Intel Core i7, 8 GB RAM machine. First, we have tested HYPNO over hundred valid formulas in E and considered extensions obtained by generalizing schemas of valid formulas by varying some crucial parameters, like the modal degree (the level of nesting of the connective), already used for testing PRONOM. For instance, we have considered the schemas (valid in all systems): obtaining encouraging results: Table 1 reports the number of timeouts of HYPNO and PRONOM over a set of valid formulas in system E. HYPNO is able to answer in less than one second on more than the 90% of the tests, whereas PRONOM is not even if we extend the time limit to 5 s. We have also tested HYPNO on randomly generated formulas, fixing different time limits, numbers of propositional variables, and levels of nesting of connectives. We have compared the performances of HYPNO with those of PRONOM, obtaining the results in Table 2 : in each pair, the first number is the percentage of timeouts of HYPNO, the second number is the percentage of timeouts of PRONOM given the fixed time limit. Also in case of formulas generated from 3 different atomic variables and with a higher level of nesting (7), HYPNO is able to answer in more than 96% of the cases within 1 s, against the 85% of PRONOM. We have repeated the experiments also for all the extensions of E considered by HYPNO: complete results can be found at http://193.51.60.97:8000/HYPNO/#experiments. Moreover, we are planning to perform more accurate tests following the approach of [8] , where randomly generated formulas can be obtained by selecting different degrees of probability about their validity. We have presented HYPNO, a prover for the cube of NNMLs based on some hypersequent calculi for these logics recently introduced. HYPNO produces both proofs and countermodels in the bi-neighbourhood semantics. Although no specific optimisation has been implemented, the performances of HYPNO are promising. In the future we intend to extend possible optimisation, in particular to minimize the size of countermodels. Moreover we intend to extend it to other non-normal modal logics in the realm of deontic and agent-ability logics. Hyper,NewHyper), 3. member(Sigma,Gamma), is_list(Sigma),member(box B,Delta), 4. list_to_ord_set(Sigma,SigmaOrd), \+member(apdR(SigmaOrd,B),Additional),!, 5. terminating_proof_search Knowledge means 'all', belief means 'most LeanTAP: lean tableau-based deduction Modal Logic Countermodel construction via optimal hypersequent calculi for non-normal modal logics PRONOM: proof-search and countermodel generation for non-normal modal logics Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi The modal logic of agency SAT-based decision procedures for classical modal logics Tableau games for coalition logic and alternating-time temporal logictheory and implementation. Master's thesis Sequent calculi and decision procedures for weak modal systems Combining monotone and normal modal logic in nested sequentswith countermodels Neighborhood Semantics for Modal Logic A modal logic for coalitional power in games On epistemic logic and logical omniscience Acknowledgements. We thank the reviewers for their careful reading that helped us to improve this paper. We are currently developing a new version of HYPNO taking into account all the suggestions about its implementation.