|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Searching for Invariants Using Temporal Resolution
Brotherston, James and Degtyarev, Anatoli and Fisher, Michael and Lisitsa, Alexei (2002) Searching for Invariants Using Temporal Resolution. In: Logic for Programming, Artificial Intelligence, and Reasoning,.
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.
Repository Staff Only: item control page