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,.

PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
167Kb

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 overview of the implementation are described.

Item Type:	Conference or Workshop Item (Paper)
Subjects:	UNSPECIFIED
ID Code:	885
Deposited By:	Dr Anatoli Degtyarev
Deposited On:	08 Nov 2007 08:33
Last Modified:	08 Nov 2007 08:33

Repository Staff Only: item control page

Accessibility | Terms and Conditions | Last Modified 01 November 2007