Automated Deduction for a Multi-Modal Logic of Time and Knowledge

Contents

In this paper we expose how to reduce a logical problem to a unification problem, and present an algorithm which solves the latter. This algorithm computes a complete set of unifiers and terminates, thus we get a terminating, sound and complete theorem prover for the logic of knowledge and time we are interested in.