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 条
  • [31] The completeness and applications of the formal system L*
    Pei, DW
    Wang, GJ
    SCIENCE IN CHINA SERIES F, 2002, 45 (01): : 40 - 50
  • [32] The completeness and applications of the formal system B
    裴道武
    王国俊
    ScienceinChina(SeriesF:InformationSciences), 2002, (01) : 40 - 50
  • [33] From Gs-monoidal to Oplax Cartesian Categories: Constructions and Functorial Completeness
    Tobias Fritz
    Fabio Gadducci
    Davide Trotta
    Andrea Corradini
    Applied Categorical Structures, 2023, 31
  • [34] STRONG COMPLETENESS IN PROFINITE GROUPS
    PLETCH, A
    PACIFIC JOURNAL OF MATHEMATICS, 1981, 97 (01) : 203 - 208
  • [35] On the finite strong completeness of NML
    Wu, Hong-Bo
    Zhang, Qiong
    Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2010, 38 (06): : 1414 - 1418
  • [36] A STRONG COMPLETENESS THEOREM FOR PRAGMATICS
    VANDERVEKEN, D
    ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1981, 27 (02): : 151 - 160
  • [37] Strong Completeness for Markovian Logics
    Kozen, Dexter
    Mardare, Radu
    Panangaden, Prakash
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2013, 2013, 8087 : 655 - 666
  • [38] ALGORITHM FOR FORMAL CALCULUS OF BOOLEAN EXPRESSIONS
    CAVADIA, IC
    REVUE FRANCAISE D AUTOMATIQUE INFORMATIQUE RECHERCHE OPERATIONNELLE, 1973, 7 (OCT): : 63 - 84
  • [39] ALGORITHM FOR FORMAL CALCULUS OF BOOLEAN EXPRESSIONS
    CAVADIA, IC
    REVUE FRANCAISE D AUTOMATIQUE INFORMATIQUE RECHERCHE OPERATIONNELLE, 1971, 5 (NB3): : 65 - 85
  • [40] INTEGRATING BOOLEAN VERIFICATION WITH FORMAL DERIVATION
    BOSE, B
    JOHNSON, SD
    PULLELA, S
    COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 139 - 146
12345