Furio Honsell and Marino Miculan
A Natural Deduction Approach to Dynamic Logics.
Natural Deduction style presentations of program logics are useful in view
of the implementation of such logics in interactive proof development environments,
based on type theory, such as LEGO, Coq, etc. In fact, ND-style systems
are the kind of systems which can take best advantage of the possibility
of reasoning ``under assumptions'' offered by proof assistants generated
by Logical Frameworks. In this paper we introduce and discuss sound and
complete proof systems in Natural Deduction style for representing various
``truth'' consequence relations of Dynamic Logic. We discuss the design
decisions which lead to adequate encodings of these logics in Coq. We derive
in Dynamic Logic a set of rules representing a ND-style system for Hoare
Logic.