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.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.