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 条
  • [31] COMPLETENESS OF HOARE-CALCULI REVISITED
    KIRKERUD, B
    BIT, 1982, 22 (04): : 402 - 418
  • [32] Alignment Completeness for Relational Hoare Logics
    Nagasamudram, Ramana
    Naumann, David A.
    2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2021,
  • [33] A propositional calculus formal deductive system LU of universal logic and its completeness
    Luo, MX
    He, HC
    FUZZY SYSTEMS AND KNOWLEDGE DISCOVERY, PT 1, PROCEEDINGS, 2005, 3613 : 31 - 41
  • [34] Completeness and decidability results for some propositional modal logic containing 'actually' operators
    Gregory, D
    JOURNAL OF PHILOSOPHICAL LOGIC, 2001, 30 (01) : 57 - 78
  • [35] Reverse Hoare Logic
    de Vries, Edsko
    Kontavas, Vasileios
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 155 - 171
  • [36] Hoare logic in the abstract
    Martin, Ursula
    Mathiesen, Erik A.
    Oliva, Paulo
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 501 - 515
  • [37] PEIRCE ALPHA GRAPHS - THE COMPLETENESS OF PROPOSITIONAL LOGIC AND THE FAST SIMPLIFICATION OF TRUTH-FUNCTIONS
    WHITE, RB
    TRANSACTIONS OF THE CHARLES S PEIRCE SOCIETY, 1984, 20 (04): : 351 - 361
  • [38] Completeness Theory for Propositional Logics
    Polacik, Tomasz
    STUDIA LOGICA, 2010, 95 (03) : 443 - 446
  • [39] STRUCTURAL COMPLETENESS OF PROPOSITIONAL CALCULUS
    POGORZELSKI, WA
    BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1971, 19 (05): : 349 - +
  • [40] THE HOARE LOGIC OF CSP, AND ALL THAT
    LAMPORT, L
    SCHNEIDER, FB
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1984, 6 (02): : 281 - 296
12345