Forward countermodel construction in modal Logic K
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino · BOA (University of Milano-Bicocca) · 2018
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 Ξ.