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 条
  • [21] On the Interval of Boolean Strong Partial Clones Containing Only Projections as Total Operations
    Couceiro, Miguel
    Haddad, Lucien
    Lagerqvist, Victor
    Roy, Biman
    2017 IEEE 47TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL 2017), 2017, : 88 - 93
  • [22] Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics
    Sano, Katsuhiko
    Stell, John G.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (243): : 105 - 121
  • [23] On the monoidal structure of matrix bi-factorizations
    Carqueville, Nils
    Runkel, Ingo
    JOURNAL OF PHYSICS A-MATHEMATICAL AND THEORETICAL, 2010, 43 (27)
  • [24] The Boolean Algebra Logic: The Soundness and Completeness Theorem
    Chen Bo
    Zhang Xingyou
    Zhang Pengfei
    Cao Cong
    Liu Wenxue
    Zhao Kang
    2017 13TH INTERNATIONAL CONFERENCE ON SEMANTICS, KNOWLEDGE AND GRIDS (SKG 2017), 2017, : 15 - 18
  • [25] Completeness of the bounded Boolean powers of orthomodular lattices
    Riecanova, Z
    ALGEBRA UNIVERSALIS, 1996, 35 (02) : 230 - 232
  • [26] Polynomial completeness criteria in finite Boolean algebras
    Romov, BA
    1996 26TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 1996, : 262 - 266
  • [27] COMPLETENESS IN SUMS OF BOOLEAN-ALGEBRAS AND LOGICS
    JANIS, V
    RIECANOVA, Z
    INTERNATIONAL JOURNAL OF THEORETICAL PHYSICS, 1992, 31 (09) : 1689 - 1697
  • [28] The completeness of the isomorphism relation for countable Boolean algebras
    Camerlo, R
    Gao, S
    TRANSACTIONS OF THE AMERICAN MATHEMATICAL SOCIETY, 2000, 353 (02) : 491 - 518
  • [29] C-Maximal Strong Partial Clones and the Inclusion Structure of Boolean Weak Bases
    Lagerkvist, Victor
    Roy, Biman
    JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2022, 38 (3-4) : 333 - 353
  • [30] Predicate Formal System ∀]Δand Its Completeness
    Ma, Ying-cang
    Liu, Huan
    QUANTITATIVE LOGIC AND SOFT COMPUTING 2010, VOL 2, 2010, 82 : 263 - 272
12345