Data di Pubblicazione:
2020
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.
Tipologia CRIS:
04A-Conference paper in volume
Elenco autori:
Dalmonte T.; Negri S.; Olivetti N.; Pozzato G.L.
Link alla scheda completa:
Link al Full Text:
Titolo del libro:
CEUR Workshop Proceedings "2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2020"
Pubblicato in: