A Cyclic Proof System for Guarded Kleene Algebra with Tests

被引：0
|
作者：
Rooduijn, Jan [1 ]
Kozen, Dexter [2 ]
Silva, Alexandra [2 ]
机构：
[1] Univ Amsterdam, Inst Log Language & Computat, Amsterdam, Netherlands
[2] Cornell Univ, Ithaca, NY USA
来源：
AUTOMATED REASONING, IJCAR 2024, PT II | 2024年 / 14740卷
基金：
荷兰研究理事会;
关键词：
Kleene Algebra; Guarded Kleene Algebra with Tests; Cyclic proofs; THEOREM;
D O I：
10.1007/978-3-031-63501-4_14
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Guarded Kleene Algebra with Tests ( GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in NLOGSPACE, whereas that of Kleene Algebra is in PSPACE.
引用
收藏
页码：257 / 275
页数：19
相关论文
共 50 条
  • [1] A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
    Kappe, Tobias
    Schmid, Todd
    Silva, Alexandra
    PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2023, 2023, 13990 : 309 - 336
  • [2] A Cut-Free Cyclic Proof System for Kleene Algebra
    Das, Anupam
    Pous, Damien
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2017, 2017, 10501 : 261 - 277
  • [3] Guarded Kleene Algebra with Tests Verification of Uninterpreted Programs in Nearly Linear Time
    Smolka, Steffen
    Foster, Nate
    Hsu, Justin
    Kappe, Tobias
    Kozen, Dexter
    Silva, Alexandra
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [4] Kleene algebra with tests
    Kozen, D
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (03): : 427 - 443
  • [5] Proof theory for Kleene algebra
    Hardin, C
    LICS 2005: 20TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE - PROCEEDINGS, 2005, : 290 - 299
  • [6] Concurrent Kleene Algebra with Tests
    Jipsen, Peter
    RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMICS 2014), 2014, 8428 : 37 - 48
  • [7] Automatic proof generation in Kleene algebra
    Worthington, James
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, 2008, 4988 : 382 - 396
  • [8] An axiomatization of arrays for Kleene algebra with tests
    Aboul-Hosn, Kamal
    RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2006, 4136 : 63 - 77
  • [9] A coalgebraic approach to Kleene algebra with tests
    Chen, HB
    Pucella, R
    THEORETICAL COMPUTER SCIENCE, 2004, 327 (1-2) : 23 - 44
  • [10] Position Automata for Kleene Algebra with Tests
    Silva, Alexandra
    SCIENTIFIC ANNALS OF COMPUTER SCIENCE, 2012, 22 (02) : 367 - 394
12345