A Proof-Checker for Dynamic Logic

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

Full description

Bibliographic Details
Main Authors: Litvintchouk, S.D., Pratt, V.R.
Language:en_US
Published: 2004
Online Access:http://hdl.handle.net/1721.1/5762