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.

A natural deduction approach to dynamic logic

HONSELL, Furio;MICULAN, Marino
1996-01-01

Abstract

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.
1996
3-540-61780-9
File in questo prodotto:
File Dimensione Formato  
TYPES95.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 319.54 kB
Formato Adobe PDF
319.54 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/682297
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 19
  • ???jsp.display-item.citation.isi??? 12
social impact