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

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.