On the completeness of propositional Hoare logic

被引：14
|
作者：
Kozen, D [1 ]
Tiuryn, J
机构：
[1] Cornell Univ, Dept Comp Sci, Ithaca, NY 14853 USA
[2] Warsaw Univ, Inst Informat, PL-02097 Warsaw, Poland
来源：
INFORMATION SCIENCES | 2001年 / 139卷 / 3-4期
关键词：
D O I：
10.1016/S0020-0255(01)00164-5
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We investigate the completeness of Hoare logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for propositional Hoare logic (PHL): all relationally valid rules {b(1)}p(1){c(1)},...,{b(n)}p(n){c(n)} / {b}p{c} are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs p; in the premises are atomic, no expressiveness assumptions are needed. (C) 2001 Elsevier Science Inc. All rights reserved.
引用
收藏
页码：187 / 195
页数：9
相关论文
共 50 条
  • [21] Soundness and Completeness of Fuzzy Propositional Logic with Three Kinds of Negation
    Pan, Zheng-Hua
    QUANTITATIVE LOGIC AND SOFT COMPUTING 2016, 2017, 510 : 71 - 79
  • [22] COMPLETENESS PROOFS FOR PROPOSITIONAL LOGIC WITH POLYNOMIAL-TIME CONNECTIVES
    CROSSLEY, JN
    SCOTT, PJ
    ANNALS OF PURE AND APPLIED LOGIC, 1989, 44 (1-2) : 39 - 52
  • [23] Completeness before post: Bernays, Hilbert, and the development of propositional logic
    Zach, R
    BULLETIN OF SYMBOLIC LOGIC, 1999, 5 (03) : 331 - 366
  • [24] Weak Completeness Theorem for Propositional Linear Time Temporal Logic
    Giero, Mariusz
    FORMALIZED MATHEMATICS, 2012, 20 (03): : 227 - 234
  • [25] A Simple Proof of Completeness and Cut-admissibility for Propositional Godel Logic
    Avron, Arnon
    JOURNAL OF LOGIC AND COMPUTATION, 2011, 21 (05) : 813 - 821
  • [26] DETERMINISTIC PROPOSITIONAL DYNAMIC LOGIC - FINITE-MODELS, COMPLEXITY, AND COMPLETENESS
    BENARI, M
    HALPERN, JY
    PNUELI, A
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (03) : 402 - 417
  • [27] ON RELATIVE COMPLETENESS OF HOARE LOGICS
    GRABOWSKI, M
    INFORMATION AND CONTROL, 1985, 66 (1-2): : 29 - 44
  • [28] Weak completeness of resolution in a linguistic truth-valued propositional logic
    Xu, Yang
    Chen, Shuwei
    Liu, Jun
    Ruan, Da
    THEORETICAL ADVANCES AND APPLICATIONS OF FUZZY LOGIC AND SOFT COMPUTING, 2007, 42 : 358 - +
  • [29] Second-order propositional modal logic: Expressiveness and completeness results
    Belardinelli, Francesco
    van der Hoek, Wiebe
    Kuijer, Louwe B.
    ARTIFICIAL INTELLIGENCE, 2018, 263 : 3 - 45
  • [30] Propositional Logic as a Propositional Fuzzy Logic
    Callejas Bedregal, Benjamin Rene
    Cruz, Anderson Paiva
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 143 : 5 - 12
12345