Invariant Serach via Temporal Resolution

This page describes an implementation of a method for a searching for invariants in the theorem proving for first-order temporal logic. The method is based on clausal temporal resolution technique [FDP01,BDFL02] and implemented in the proof planning system $\lambda Clam$ using the advantages of the higher-order logical programming language $\lambda Prolog$. Invariant Search via Temporal Resolution