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 |
Externí odkaz: |