- Abstract:
-
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 an overview of the implementation are described.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0144,
- author = {
James Brotherston
and Alexei Lisitsa
and Michael Fisher
and Anatoli Degtyarev
},
- title = {Searching for Invariants using Temporal Resolution},
- year = 2002,
- month = {Aug},
- }
|
