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 E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology ofand 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.
PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics
Negri S.;
2019-01-01
Abstract
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 E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology ofand 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
