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
Ferrari, Mauro
;Fiorentini, Camillo;Fiorino, Guido
2018-01-01
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 in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
