UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Searching for invariants using temporal resolution

Brotherston, J; Degtyarev, A; Fisher, M; Lisitsa, A; (2002) Searching for invariants using temporal resolution. In: (pp. pp. 86-101).

Full text not available from this repository.


© Springer-Verlag Berlin Heidelberg 2002. 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.

Type: Proceedings paper
Title: Searching for invariants using temporal resolution
ISBN: 3540000100
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1353147
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item