Proof-search and countermodel generation for non-normal modal logics: The theorem prover PRONOM
| Autor: | Nicola Olivetti, Gian Luca Pozzato, Tiziano Dalmonte, Sara Negri |
|---|---|
| Přispěvatelé: | Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Helsingin yliopisto = Helsingfors universitet = University of Helsinki, Università degli studi di Genova = University of Genoa (UniGe), Logique, Interaction, Raisonnement et Inférence, Complexité, Algèbre (LIRICA), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Università degli studi di Torino = University of Turin (UNITO), ANR-16-CE91-0002,TICAMORE,Traduction et Découverte des Calculs pour les logiques Modales et dérivées(2016) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computer science
010102 general mathematics Labelled sequent calculi Proof search [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 02 engineering and technology Countermodel generation 01 natural sciences Non-normal modal logics Theorem proving [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] Automated theorem proving Modal TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Calculus 020201 artificial intelligence & image processing Non normality 0101 mathematics |
| Zdroj: | Intelligenza Artificiale Intelligenza Artificiale, 2021, 14 (2), pp.215-229. ⟨10.3233/IA-200052⟩ |
| ISSN: | 1724-8035 2211-0097 |
| DOI: | 10.3233/IA-200052⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|