A Natural Deduction Approach to Dynamic Logic
A Natural Deduction Approach to Dynamic Logic
复制标题
动态逻辑的自然演绎方法
DOI：
10.1007/3-540-61780-9_69
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Marino Miculan
中科院分区：
文献类型：
--
作者：
F. Honsell;Marino Miculan
基于类型理论（例如LEGO，COQ等）在交互式证明开发环境中实现此类逻辑的自然扣除样式演示对于在交互式证明开发环境中的实现非常有用。最好利用逻辑框架在本文中产生的“假设下的假设”的可能性讨论我们在COQ中的这些逻辑的适当编码的设计决策。
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.