We present an implementation of an interactive theorem prover for the basic tense logic K_t, 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 K_t 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.
展开▼
