论文标题
具有归纳定义和理论推理的分离逻辑的证明程序
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
论文作者
论文摘要
提出了一个证明程序，以序列的微积分的精神来检查分离逻辑公式之间的有效性，结合了归纳定义的谓词表示有界树宽度和理论推理的结构。微积分是合理而完整的，从某种意义上说，如果序列有效，则该序列是（可能是无限的）证明树。我们表明，该过程在以下两种情况下终止：（i）定义在支出左侧的谓词的归纳规则终止时，在这种情况下，证明树总是有限的。 （ii）当该理论为空时，在这种情况下，每个有效的序列都承认一个有理的证明树，其中证明树中发生的成对隔离序列的总数是双重指数的W.R.T. \最终后续的大小。
A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoted structures of bounded tree width and theory reasoning. The calculus is sound and complete, in the sense that a sequent is valid iff it admits a (possibly infinite) proof tree. We show that the procedure terminates in the two following cases: (i) When the inductive rules that define the predicates occurring on the left-hand side of the entailment terminate, in which case the proof tree is always finite. (ii) When the theory is empty, in which case every valid sequent admits a rational proof tree, where the total number of pairwise distinct sequents occurring in the proof tree is doubly exponential w.r.t.\ the size of the end-sequent.
