# HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)

- 188 Downloads

## Abstract

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 \(\mathbf {E}\) and its extensions with axioms M, N, and C. It is inspired by the methodology of Open image in new window, 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.

## Keywords

Non-normal modal logics Hypersequent calculi Prolog## 1 Introduction

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 \(\mathbf {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 \(\mathbf {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 \([\forall \forall ]\) and the \([\exists \forall ]\) modality; its \([\exists \forall ]\) fragment coincides with the logic \(\mathbf {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/.

## 2 Axioms, Semantics, and Hypersequent Calculi

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 \(\mathsf {Atm}\), the formulas of the language \(\mathcal L\) of NNMLs are built as follows: \(A\, {:}{:}= p \mid \bot \mid \top \mid A \vee A \mid A \wedge A \mid A \rightarrow A \mid \Box A\), where \(p\in \mathsf {Atm}\). The minimal NNML \(\mathbf {E}\) is defined in \(\mathcal L\) by extending classical propositional logic with the rule RE below. The systems of the classical cube are then obtained by adding to \(\mathbf {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 \(\mathbf {EMCN}\) coincides with normal modal logic \(\mathbf {K}\).
Open image in new window

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.

### Definition 1

A *bi-neighbourhood model* is a tuple \(\mathcal M= \langle \mathcal W, \mathcal N_b, \mathcal V\rangle \), where \(\mathcal W\) is a non-empty set of worlds, \(\mathcal V\) is a valuation function, and \(\mathcal N_b\) is a bi-neighbourhood function \(\mathcal W\longrightarrow \mathcal P(\mathcal P(\mathcal W)\times \mathcal P(\mathcal W))\). We say that \(\mathcal M\) is a *M-model* if \((\alpha , \beta )\in \mathcal N_b(w)\) implies \(\beta =\emptyset \), it is a *N-model* if for all \(w\in \mathcal W\) there is \(\alpha \subseteq \mathcal W\) such that \((\alpha , \emptyset )\in \mathcal N_b(w)\), and it is a *C-model* if \((\alpha _1, \beta _1), (\alpha _2, \beta _2)\in \mathcal N_b(w)\) implies \((\alpha _1\cap \alpha _2, \beta _1\cup \beta _2)\in \mathcal N_b(w)\). The forcing relation for boxed formulas is as follows: \(\mathcal M, w\Vdash \Box A\) if and only if there is \((\alpha , \beta )\in \mathcal N_b(w) \) s.t. \(\alpha \subseteq [A]\subseteq \mathcal W\setminus \beta \), where [*A*] denotes the truth set of *A* in \(\mathcal M\).

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 \(\mathbf {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 \(\langle \varSigma \rangle \), where \(\varSigma \) is a multiset of formulas of \(\mathcal L\). A *sequent* is a pair \({\varGamma \Rightarrow \varDelta }\), where \(\varGamma \) is a multiset of formulas and blocks, and \(\varDelta \) is a multiset of formulas. A *hypersequent* is a multiset \(S_1 \mid ... \mid S_n\), where \(S_1, ..., S_n\) are sequents. Single sequents can be interpreted into the language as: \( i(A_1, ..., A_n, \langle \varSigma _1 \rangle , ..., \langle \varSigma _m \rangle \Rightarrow B_1, ..., B_k) = \bigwedge _{i\le n}A_i \wedge \bigwedge _{j \le m}\Box \bigwedge \varSigma _j \rightarrow \bigvee _{\ell \le k}B_\ell \;. \) We say that a sequent *S* is *valid* in a bi-neighbourhood model \(\mathcal M\) (written \(\mathcal M\,\models \,S\)) if for all \(w\in \mathcal M\), \(\mathcal M, w\Vdash i(S)\). Moreover, a hypersequent *H* is *valid* in \(\mathcal M\) (\(\mathcal M\,\models \,H\)) if \(\mathcal M\,\models \,S\) for some \(S\in H\), and it is valid in (M/C/N-)models if it is valid in all models of that kind.

*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: \(\mathcal H_{\mathsf E}\) := propositional rules + \(\Box _\mathsf L\) + \(\Box _\mathsf R\) + \(\Rrightarrow _1\) + \(\Rrightarrow _2\); \(\mathcal H_{\mathsf {EN}}\) := \(\mathcal H_{\mathsf E}\) + \(\mathsf N\); \(\mathcal H_{\mathsf {EC}}\) := \(\mathcal H_{\mathsf E}\) + \(\mathsf C\); \(\mathcal H_{\mathsf {ECN}}\) := \(\mathcal H_{\mathsf E}\) + \(\mathsf C\) + \(\mathsf N\); \(\mathcal H_{\mathsf M}\) := propositional rules + \(\Box _\mathsf L\) + \({}_{\mathsf M}\Box _\mathsf R\); \(\mathcal H_{\mathsf {MN}}\) := \(\mathcal H_{\mathsf M}\) + \(\mathsf N\); \(\mathcal H_{\mathsf {MC}}\) := \(\mathcal H_{\mathsf M}\) + \(\mathsf C\); and \(\mathcal H_{\mathsf {MCN}}\) := \(\mathcal H_{\mathsf M}\) + \(\mathsf C\) + \(\mathsf N\). In the following, we denote by \(\mathcal H_{\mathsf E^{\star }}\) any extension of \(\mathcal H_{\mathsf E}\).

## 3 Design of HYPNO

The prover HYPNO implements the calculi of Fig. 1. It is inspired by the “lean” methodology of Open image in new window [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”.

is used to represent the hypersequent \(\Box (A \wedge C), \langle \top \rangle , \langle A, C \rangle \Rightarrow A, B, A \vee B, \Box B \mid P \Rightarrow P\), to which the rules \(\mathsf N\), \(\vee _\mathsf R\) and \(\Box _\mathsf R\) have been already applied, the last one by using the block \( \langle A, C \rangle \) and the formula \(\Box B\) as the principal formulas. In turn, no rule has been applied to \(P \Rightarrow P\) (the list Additional is empty).

*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:

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 \(\Box _\mathsf R\) has been already applied on that sequent by using \(\Box B\) and the block \(\varSigma \), 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 \(\varSigma \Rightarrow B\) and \(B \Rrightarrow \varSigma \) respectively. Since the rule is invertible, Prolog cut ! is used in line 4 to eventually block backtracking.

*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 \(\varSigma \) in the left hand side and of a boxed formula \(\Box B\) in the right hand side of a sequent:

HYPNO will first try to build a countermodel by considering the left premise of \(\Box _\mathsf R\), whence recursively invoking the predicate build_saturated_branch on the premise with the sequent \(\varSigma \Rightarrow B\). In case of a failure, it will carry on the saturation process by using the right premise of \(\Box _\mathsf R\) with the sequent \(B \Rrightarrow \varSigma \).

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 \(\mathbf {E}\) is very similar: given the modularity of the calculi \(\mathcal H_{\mathsf E^{\star }}\), 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 Open image in new window source file. Otherwise, a countermodel falsifying the initial formula is displayed. Prolog source codes are also available.

## 4 Performance of HYPNO

Percentage of timeouts over valid formulas in \(\mathbf {E}\).

System | 0,1 ms | 1 ms | 100 ms | 1 s | 5 s |
---|---|---|---|---|---|

HYPNO | 91,50% | 78,91% | 28,23% | 9,52% | 5,78% |

PRONOM | 85,71% | 77,55% | 57,82% | 31,16% | 19,80% |

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.

Percentage of timeouts in 5000 random tests (system \(\mathbf {E}\)).

Vars/Depth | 1 ms | 10 ms | 1 s | 10 s |
---|---|---|---|---|

3 vars - depth 5 | 4–5,58% | 0,78–1,76% | 0,02–0,48% | 0–0,22% |

3 vars - depth 7 | 23,78–25,18% | 10,86–20,16% | 3,16–14,40% | 2,02–12% |

7 vars - depth 10 | 45,22–44,94% | 34,36–42,36% | 19,06–30,30% | 16,06–20,34% |

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 \(\mathbf {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.

## 5 Conclusions

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.

## Footnotes

## Notes

### 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.

## References

- 1.Askounis, D., Koutras, C.D., Zikos, Y.: Knowledge means ‘all’, belief means ‘most’. J. Appl. Non-Class. Log.
**26**(3), 173–192 (2016). https://doi.org/10.1080/11663081.2016.1214804MathSciNetCrossRefzbMATHGoogle Scholar - 2.Beckert, B., Posegga, J.: LeanTAP: lean tableau-based deduction. J. Autom. Reasoning
**15**(3), 339–358 (1995). https://doi.org/10.1007/BF00881804CrossRefzbMATHGoogle Scholar - 3.Chellas, B.F.: Modal Logic. Cambridge University Press, Cambridge (1980)CrossRefGoogle Scholar
- 4.Dalmonte, T., Lellmann, B., Olivetti, N., Pimentel, E.: Countermodel construction via optimal hypersequent calculi for non-normal modal logics. In: Artemov, S., Nerode, A. (eds.) LFCS 2020. LNCS, vol. 11972, pp. 27–46. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-36755-8_3CrossRefGoogle Scholar
- 5.Dalmonte, T., Negri, S., Olivetti, N., Pozzato, G.L.: PRONOM: proof-search and countermodel generation for non-normal modal logics. In: Alviano, M., Greco, G., Scarcello, F. (eds.) AI*IA 2019. LNCS (LNAI), vol. 11946, pp. 165–179. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-35166-3_12 CrossRefGoogle Scholar
- 6.Dalmonte, T., Olivetti, N., Negri, S.: Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi. In: Proceedings of AiML 12, pp. 159–178. College Publications (2018)Google Scholar
- 7.Elgesem, D.: The modal logic of agency. Nord. J. Philos. Log.
**2**(2), 1–46 (1997)Google Scholar - 8.Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Autom. Reasoning
**28**(2), 143–171 (2002). https://doi.org/10.1023/A:1015071400913MathSciNetCrossRefzbMATHGoogle Scholar - 9.Hansen, H.: Tableau games for coalition logic and alternating-time temporal logic-theory and implementation. Master’s thesis, University of Amsterdam (2004)Google Scholar
- 10.Lavendhomme, R., Lucas, T.: Sequent calculi and decision procedures for weak modal systems. Studia Logica
**66**, 121–145 (2000). https://doi.org/10.1023/A:1026753129680MathSciNetCrossRefzbMATHGoogle Scholar - 11.Lellmann, B.: Combining monotone and normal modal logic in nested sequents – with countermodels. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 203–220. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29026-9_12CrossRefzbMATHGoogle Scholar
- 12.Pacuit, E.: Neighborhood Semantics for Modal Logic. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-319-67149-9CrossRefzbMATHGoogle Scholar
- 13.Pauly, M.: A modal logic for coalitional power in games. J. Log. Comput.
**12**(1), 149–166 (2002)MathSciNetCrossRefGoogle Scholar - 14.Vardi, M.Y.: On epistemic logic and logical omniscience. In: Theoretical Aspects of Reasoning About Knowledge, pp. 293–305. Elsevier (1986)Google Scholar