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 Ξ.
Ferrari, M., Fiorentini, C., Fiorin, O. (2018). Forward countermodel construction in modal Logic K. In Proceedings of the 33rd Italian Conference on Computational Logic, Bolzano, Italy, September 20-22, 2018 (pp.75-81). CEUR-WS.
Forward countermodel construction in modal Logic K
Fiorino. G
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 | |
|---|---|---|---|
|
paper8.pdf
Solo gestori archivio
Tipologia di allegato:
Publisher’s Version (Version of Record, VoR)
Dimensione
543.2 kB
Formato
Adobe PDF
|
543.2 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
