Wahab, Matthew (1996) The semantics of TLA on the PVS theorem prover. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)

Preview

PDF (Department of Computer Science Research Report) WRAP_cs-rr-317.pdf - Other - Requires a PDF viewer. Download (226Kb) | Preview

Request Changes to record.

Abstract

An implementation of Lamport's Temporal Logic of Actions (TLA) on a higher order logic theorem prover is described. TLA is a temporal logic, for which a syntax and semantics are defined, based on an action logic which is represented by higher order functions. The temporal logic includes quantifiers for variables with constant values and for variables whose values change over time. The semantics of the latter depend on an auxiliary function which cannot be defined by primitive recursion and an alternative is given based on the Hilbert e operator.

Item Type:	Report
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions:	Faculty of Science, Engineering and Medicine > Science > Computer Science
Library of Congress Subject Headings (LCSH):	Automatic theorem proving, Logic, Computer programs -- Mathematical models
Series Name:	Department of Computer Science research report
Publisher:	University of Warwick. Department of Computer Science
Official Date:	4 October 1996
Dates:	Date Event 4 October 1996 Completion
Number:	Number 317
Number of Pages:	17
DOI:	CS-RR-317
Institution:	University of Warwick
Theses Department:	Department of Computer Science
Status:	Not Peer Reviewed
Publication Status:	Unpublished
Related URLs:	Organisation

Request changes or add full text files to a record

Repository staff actions (login required)

View Item

Downloads