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.
Work partially supported by the Esprit BRP no.6453, Types for Proofs and Programs, and italian MURST 40%–60% grants. Some of the results of this papers have been communicated by the second author at the TYPES Annual Meeting in Båstad, 1994.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt. Ten years of Hoare's logic: A survey —part I. ACM Transactions on Programming Languages and Syms, 3(4):431–483, Oct. 1981.
A. Avron. Simple consequence relations. Inform. Comput., 92:105–139, Jan. 1991.
A. Avron, F. Honsell, I. A. Mason, and R. Pollack. Using Typed Lambda Calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309–354, 1992.
R. Burstall and F. Honsell. Operational semantics in a natural deduction setting. In Huet and Plotkin [13], pages 185–214.
T. Coquand and G. Huet. The calculus of constructions. Information and Control, 76:95–120, 1988.
M. J. C. Gordon. Mechanizing program logics in higher order logic. In P. A. Subrahmanyam and G. Birtwistle, editors, Current Trends in Hardware Verification and Automated Theorem Prover, pages 387–439. Springer-Verlag, 1989.
D. Harel. First-Order Dynamic Logic. No.68 in LNCS. Springer-Verlag, 1979.
D. Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 497–604. Reidel, 1984.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143–184, Jan. 1993.
M. Heisel, W. Reif, and W. Stephan. A dynamic logic for program verification. In A. Meyer and M. Taitslin, editors, Proc. of LFCS (Logic at Botik), number 363 in Lecture Notes in Computer Science, pages 134–145. Springer-Verlag, 1989.
F. Honsell and M. Miculan. Encoding program logics in type theories. In J. Despeyroux, editor, Deliverables of the TYPES Workshop Proving Properties of Programming Languages, Sophia-Antipolis, Sept. 1993.
F. Honsell, M. Miculan, and C. Paravano. Encoding modal logics in Logical Frameworks. To appear, 1996.
G. Huet and G. Plotkin, editors. Logical Frameworks. CUP, June 1990.
INRIA, Rocquencourt. The Coq Proof Assistant Reference Manual, July 1995.
D. Kozen and J. Tiuryn. Logics of Programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 789–840. North Holland, 1990.
Z. Luo, R. Pollack, and P. Taylor. How to use LEGO (A Preliminary User's Manual). Department of Computer Science, University of Edinburgh, Oct. 1989.
A. R. Meyer and J. Y. Halpern. Axiomatic definition of programming languages: A theoretical assessment. J. ACM, 29(2):555–576, Apr. 1982.
S. Michaylov and F. Pfenning. Natural Semantics and some of its Meta-Theory in Elf. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, number 596 in LNAI, pages 299–344, Stockolm, Sweden, Jan. 1991. Springer-Verlag.
M. Miculan. The expressive power of structural operational semantics with explicit assumptions. In H. Barendregt and T. Nipkow, editors, Proceedings of TYPES'93, number 806 in LNCS, pages 292–320. Springer-Verlag, 1994.
M. Miculan. Encoding Logical Theories of Programs. PhD thesis, Università di Pisa, 1997. To appear.
F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322. IEEE, June 1989.
D. Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965.
W. Reif. The KIV system: Systematic construction of verified software. In D. Kapur, editor, Proc. of CADE-11, number 607 in Lecture Notes in Computer Science, pages 753–757. Springer-Verlag, 1992.
J. C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39–46, Tucson, Oct. 1978. The Association for Computing Machinery.
C. Stirling. Logics for While Programs: Algorithmic/Dynamic Logics. Unpublished notes, 1985.
C. Stirling. Modal and Temporal Logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 477–563. Oxford University Press, 1992.
B. Werner. Une théorie des constructions inductives. PhD thesis, Université Paris 7, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Honsell, F., Miculan, M. (1996). A natural deduction approach to dynamic logic. In: Berardi, S., Coppo, M. (eds) Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science, vol 1158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61780-9_69
Download citation
DOI: https://doi.org/10.1007/3-540-61780-9_69
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61780-8
Online ISBN: 978-3-540-70722-6
eBook Packages: Springer Book Archive