Automated Mutual Explicit Induction Proof in Separation Logic
Automated Mutual Explicit Induction Proof in Separation Logic
复制标题
DOI：
10.1007/978-3-319-48989-6_40
复制
发表时间：
2016-09
期刊：
影响因子：
--
通讯作者：
Quang-Trung Ta;T. Le;Siau-Cheng Khoo;W. Chin
中科院分区：
文献类型：
--
作者：
Quang-Trung Ta;T. Le;Siau-Cheng Khoo;W. Chin
我们提出了一个基于序列的演绎系统，利用数学归纳法自动证明分离逻辑中的蕴涵。我们的技术，称为相互显式归纳证明，是诺特归纳的一个实例。具体地说，我们在分离逻辑模型的良基关系上提出了一种新的归纳原理，并遵循显式归纳方法将该原理实现为推理规则，从而使其易于集成到演绎系统中。我们还支持mutualinduction，隐式归纳的一个自然特征，在证明搜索过程中导出的目标蕴涵和其他蕴涵可以用作假设来证明对方。我们已经实现了一个原型证明，并评估它的基准手工制作的蕴涵以及基准分离逻辑的竞争。
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, calledmutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model, and follow theexplicitinduction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also supportmutualinduction, a natural feature of implicit induction, where the goal entailment and other entailments derived during the proof search can be used as hypotheses to prove each other. We have implemented a prototype prover and evaluated it on a benchmark of handcrafted entailments as well as benchmarks from a separation logic competition.