Automated Cyclic Entailment Proofs in Separation Logic

被引：0
|
作者：
Brotherston, James [1 ]
Distefano, Dino [2 ]
Petersen, Rasmus Lerchedahl [2 ]
机构：
[1] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England
[2] Univ London Queen Mary, Dept Comp Sci, London E1 4NS, England
来源：
AUTOMATED DEDUCTION - CADA-23 | 2011年 / 6803卷
基金：
英国工程与自然科学研究理事会;
关键词：
SHAPE-ANALYSIS; VERIFICATION;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present a general automated proof procedure, based upon cyclic proof, for inductive entailments in separation logic. Our procedure has been implemented via a deep embedding of cyclic proofs in the HOL Light theorem prover. Experiments show that our mechanism is able to prove a number of non-trivial entailments involving inductive predicates.
引用
下载
收藏
页码：131 / +
页数：3
相关论文
共 50 条
  • [41] Logic of proofs with substitution
    N. M. Rubtsova
    Mathematical Notes, 2007, 82 : 816 - 826
  • [42] The logic of proofs, semantically
    Fitting, M
    ANNALS OF PURE AND APPLIED LOGIC, 2005, 132 (01) : 1 - 25
  • [43] Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules
    Echenim, Mnacho
    Iosif, Radu
    Peltier, Nicolas
    INFORMATION PROCESSING LETTERS, 2022, 173
  • [44] MATHEMATICAL LOGIC AND THE SUBSTITUTIONAL ACCOUNT OF ENTAILMENT
    DALE, AJ
    ANALYSIS, 1980, 40 (04) : 203 - 205
  • [45] Logic of approximate entailment in quasimetric spaces
    Vetterlein, Thomas
    INTERNATIONAL JOURNAL OF APPROXIMATE REASONING, 2015, 64 : 39 - 53
  • [46] On rational entailment for Propositional Typicality Logic
    Booth, Richard
    Casini, Giovanni
    Meyer, Thomas
    Varzinczak, Ivan
    ARTIFICIAL INTELLIGENCE, 2019, 277
  • [47] On Automated Lemma Generation for Separation Logic with Inductive Definitions
    Enea, Constantin
    Sighireanu, Mihaela
    Wu, Zhilin
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 80 - 96
  • [48] Automated Mutual Explicit Induction Proof in Separation Logic
    Ta, Quang-Trung
    Le, Ton Chanh
    Khoo, Siau-Cheng
    Chin, Wei-Ngan
    FM 2016: FORMAL METHODS, 2016, 9995 : 659 - 676
  • [49] Abstract cyclic proofs
    Afshari, Bahareh
    Wehr, Dominik
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2024, 34 (07) : 552 - 577
  • [50] Automated Constructivization of Proofs
    Gilbert, Frederic
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2017), 2017, 10203 : 480 - 495
12345