PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics

Autor: Sara Negri, Nicola Olivetti, Gian Luca Pozzato, Tiziano Dalmonte
Přispěvatelé: Dalmonte, Tiziano, Logique, Interaction, Raisonnement et Inférence, Complexité, Algèbre (LIRICA), Laboratoire d'Informatique et Systèmes (LIS), 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)-Aix Marseille Université (AMU), Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU), University of Helsinki, University of Turin, 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), 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 Torino = University of Turin (UNITO)
Rok vydání: 2019
Předmět:
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Semantics (computer science)
0102 computer and information sciences
02 engineering and technology
01 natural sciences
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Prolog
Tree (descriptive set theory)
Labelled sequent calculi
Non-normal modal logics
Theorem proving
0202 electrical engineering
electronic engineering
information engineering

Sequent
Axiom
Mathematics
computer.programming_language
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Algebra
Automated theorem proving
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Modal
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
020201 artificial intelligence & image processing
computer
Generator (mathematics)
Zdroj: Lecture Notes in Computer Science ISBN: 9783030351656
AI*IA
AIIA 2019: 18th International Conference of the Italian Association for Artificial Intelligence
AIIA 2019: 18th International Conference of the Italian Association for Artificial Intelligence, Nov 2019, Rende, Italy
DOI: 10.1007/978-3-030-35166-3_12
Popis: 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 \(\mathbf {E}\) and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of Open image in new window and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having that formula as a root in the labelled calculi, 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