Forward countermodel construction in modal Logic K

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 Ξ.