A mechanisation of classical modal tense logics using isabelle

Abstract

We present an implementation of an interactive theorem prover for the basic tense logic Kt, and many of its extensions, using the generic proof assistant Isabelle. The novelty of the implementation is that we use a Display Logic formalism of kt as opposed to a traditional Gentzen system. The prover is intended to assist in meta-theoretical studies of tense logics rather than to be a fast theorem prover. Since Display Logic is a generic way to capture multi-modal logics, our implementation can be trivially extended to handle the multi-modal logics of “time”, “knowledge”, “intentions”, “desires” and “beliefs” which are used in Artificial Intelligence research. Show more