【24h】

On the Completeness of Dynamic Logic

机译:论动态逻辑的完备性

获取原文
获取原文并翻译 | 示例

摘要

The impossibility of semantically complete deductive calculi for logics for imperative programs has led to the study of two alternative approaches to completeness: "local" semantic completeness on the one hand (Cook's relative completeness, Harel's Arithmetical completeness), and completeness with respect to other forms of reasoning about programs, on the other. However, local semantic completeness is problematic on several counts, whereas proof theoretic completeness results often involve ad hoc ingredients, such as formal theories for the natural numbers.rnThe notion of inductive completeness, introduced in [18], provides a generic proof theoretic framework which dispenses with extraneous ingredients, and yields local semantic completeness as a corollary.rnHere we prove that (first-order) Dynamic Logic for regular programs (DL) is inductively complete: a DL-formula φ is provable in (the first-order variant of) Pratt-Segerberg deductive calculus DL iff φ, is provable in first-order logic from the inductive theory for program semantics. The method can be adapted to yield the schematic relative completeness of DL: if S is an expressive structure, then every formula true in S is provable from the axiom-schemas that are valid in S. Harel's Completeness Theorem falls out then as a special case.
机译:祈使程序逻辑的语义上完全演绎演算的不可能导致了两种方法来研究完整性:一方面是“局部”语义完整性(库克的相对完整性,哈雷尔的算术完整性),以及其他形式的完整性另一方面,关于程序的推理。然而,局部语义完整性在很多方面都是有问题的,而证明理论完整性的结果通常涉及一些特殊的成分,例如自然数的形式论。[18]中引入的归纳完整性概念提供了一个通用的证明理论框架。此处我们证明正则程序(DL)的(一阶)动态逻辑是归纳完整的:DL公式φ可证明(的一阶变体) )Pratt-Segerberg演绎演算DL iffφ,是根据程序语义的归纳理论在一阶逻辑中得到证明的。该方法可以适用于得出DL的示意性相对完整性:如果S是一个表达结构,则S中的每个公式都可以从S中有效的公理方案中得到证明。Harel完整性定理不存在,然后作为特例。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号