The formal strong completeness of partial monoidal Boolean BI

被引：12
|
作者：
Larchey-Wendling, Dominique [1 ]
机构：
[1] LORIA CNRS, Campus Sci,BP 239, Vandoeuvre Les Nancy, France
来源：
JOURNAL OF LOGIC AND COMPUTATION | 2016年 / 26卷 / 02期
关键词：
Boolean BI logic; labelled tableaux; completeness; PROOF THEORY;
D O I：
10.1093/logcom/exu031
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This article presents a self-contained proof of the strong completeness of the labelled tableaux method for partial monoidal Boolean BI: if a formula has no tableau proof then there exists a counter-model for it which is simple. Simple counter-models are those which are generated from the specific constraints that occur during the tableaux proof-search process. As a companion to this article, we provide a complete formalization of this result in Coq and discuss some of its implementation details. The Coq code is distributed under a free software license and is accessible at ext-link-type="uri" xlink:href="http://www.loria.fr/similar to larchey/BBI"
引用
收藏
页码：605 / 640
页数：36
相关论文
共 50 条
12345