A Proof-Checker for Dynamic Logic

dc.creator	Litvintchouk, S.D.
dc.creator	Pratt, V.R.
dc.date	2004-10-01T20:34:26Z
dc.date	2004-10-01T20:34:26Z
dc.date	1977-06-01
dc.date.accessioned	2013-10-09T02:41:06Z
dc.date.available	2013-10-09T02:41:06Z
dc.date.issued	2013-10-09
dc.identifier	AIM-429
dc.identifier	http://hdl.handle.net/1721.1/5762
dc.identifier.uri	http://koha.mediu.edu.my:8181/xmlui/handle/1721
dc.description	We consider the problem of getting a computer to follow reasoning conducted in dynamic logic. This is a recently developed logic of programs that subsumes most existing first-order logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness. Dynamic logic is more closely related to classical first-order logic than any other proposed logic of programs. This simplifies the design of a proof-checker for dynamic logic. Work in progress on the implementation of such a program is reported on, and an example machine-checked proof is exhibited.
dc.format	19 p.
dc.format	6158778 bytes
dc.format	4308578 bytes
dc.format	application/postscript
dc.format	application/pdf
dc.language	en_US
dc.relation	AIM-429
dc.title	A Proof-Checker for Dynamic Logic

Files in this item

Files	Size	Format	View
There are no files associated with this item.