KSP: A Resolution-Based Prover for Multimodal K

摘要

In this paper, we describe an implementation of a hyperresolution-based calculus for the propositional basic multimodal logic, K_n. The prover was designed to support experimentation with different combinations of refinements for its basic calculus: it is primarily based on the set of support strategy, which can then be combined with other refinements, simplification techniques and different choices for the underlying normal form and clause selection. The prover allows for both local and global reasoning. We show experimental results for different combinations of strategies and comparison with existing tools.