Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Searching for Invariants using Temporal Resolution
Authors: James Brotherston ; Alexei Lisitsa ; Michael Fisher ; Anatoli Degtyarev
Date:Aug 2002
Publication Title:LPAR'02
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.
2002 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { James Brotherston and Alexei Lisitsa and Michael Fisher and Anatoli Degtyarev },
title = {Searching for Invariants using Temporal Resolution},
year = 2002,
month = {Aug},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh