Testing an implementation of a temporal logic language

Axiomatic presentations contain a great deal of information that can be used in the testing of an implementation. We describe how we rested an implementation of a temporal logical system, specifically an implementation of an extension [2] of the language Temporal Prolog [1]. However, this testing approach generalizes to any system specified using a Hilbert model (i.e. a system described using a set of axioms and inference rules) and implemented as a Prolog program. Our approach allowed US to discover some errors in the program. The necessary background information on temporal logic and specification-based testing has been included in order to make the exposition as self-contained as possible.