In this work we briefly summarize our recent contributions in the field of proof methods, theorem proving and countermodel generation for non-normal modal logics. We first recall some labelled sequent calculi for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. Then, we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof in the labelled calculi, otherwise it is able to extract a model falsifying it from an open, saturated branch.

Theorem proving for non-normal modal logics

Pozzato G. L.
2020-01-01

Abstract

In this work we briefly summarize our recent contributions in the field of proof methods, theorem proving and countermodel generation for non-normal modal logics. We first recall some labelled sequent calculi for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. Then, we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof in the labelled calculi, otherwise it is able to extract a model falsifying it from an open, saturated branch.
2020
2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2020
Bolzano (virtual)
2020
CEUR Workshop Proceedings "2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2020"
CEUR-WS
2785
17
22
http://ceur-ws.org/Vol-2785/paper3.pdf
Dalmonte T.; Negri S.; Olivetti N.; Pozzato G.L.
File in questo prodotto:
File Dimensione Formato  
paper3.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 530.33 kB
Formato Adobe PDF
530.33 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1795581
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact