The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a formula in the modal logic K. To this aim, we design a forward calculus to check the K-satisfiability of a set of modal formulas. From a derivation of Ξ, we can extract a Kripke model of Ξ.
Forward countermodel construction in modal Logic K / M. Ferrari, C. Fiorentini, G. Fiorino (CEUR WORKSHOP PROCEEDINGS). - In: CILC 2018 : Italian Conference on Computational Logic / [a cura di] P. Felli, M. Montali. - [s.l] : CEUR-WS, 2018. - pp. 75-81 (( Intervento presentato al 33. convegno Italian Conference on Computational Logic tenutosi a Bolzano nel 2018.
Forward countermodel construction in modal Logic K
C. Fiorentini;
2018
Abstract
The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a formula in the modal logic K. To this aim, we design a forward calculus to check the K-satisfiability of a set of modal formulas. From a derivation of Ξ, we can extract a Kripke model of Ξ.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2018_cilc.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
543.2 kB
Formato
Adobe PDF
|
543.2 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
