Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM

Issue title: Selected and revised papers from the 18th International Conference of the Italian Association for Artificial Intelligence

Guest editors: Mario Alviano, Gianluigi Greco and Francesco Scarcello

Article type: Research Article

Authors: Dalmonte, Tiziano^b | Negri, Sara^{c; d} | Olivetti, Nicola^b | Pozzato, Gian Luca^{a; *}

Affiliations: [a] Dipartimento di Informatica, Università di Torino, Torino, Italy | [b] Aix-Marseille University, Université de Toulon, CNRS, Marseille Cedex, France | [c] Department of Philosophy, University of Helsinki, Helsinki, Finland | [d] Dipartimento di Matematica, Università di Genova, Genova, Italy

Correspondence: [*] Corresponding author: Gian Luca Pozzato, Dipartimento di Informatica, Università di Torino, c.so Svizzera 185, 10149 Torino, Italy. E-mail: gianluca.pozzato@unito.it.

Abstract: In this work we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of leanTAP and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having a sequent with an empty left-hand side and containing only that formula on the right-hand side as a root, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising.

Keywords: Non-normal modal logics, Labelled sequent calculi, Theorem proving, Countermodel generation

DOI: 10.3233/IA-200052

Journal: Intelligenza Artificiale, vol. 14, no. 2, pp. 215-229, 2020