In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method
for searching for invariants, and so is suitable for mechanising a wide class of temporal problems. We demonstrate that this
scheme of searching for invariants can be also applied to a class of multi-predicate induction problems represented by mutually
recursive definitions. Completeness of the approach, examples of the application of the scheme, and overview of the implementation
are described.
Work supported by EPSRC grants GR/M46624, GR/M46631 and GR/R45367.