Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

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

[img]PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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)
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