KSP: A Resolution-based Prover for Multimodal K, Abridged Report.

We briefly describe an implementation of a hyperresolution-based calculus for the propositional basic multimodal logic, Kn. The prover, KSP, which allows for both local and global reasoning, is designed to support experimentation with different combinations of refinements for its basic calculus. We present an experimental evaluation that compares K S P with a range of existing reasoners for Kn.