A Resolution-Based Prover for Normal Modal Logics

ABSTRACT. WWe present a prototype tool for automated reasoning for multimodal normal logics where combinations of the axioms K, T, D, B, 4, and 5 hold. The theorem prover is based on previous work on resolution calculi for such logics. We briefly present the syntax, the semantics, and the calculus for the basic normal logic together with the inference rules for dealing with each specific axiom. We then give details of the implementation of the prover and discuss future work.