UNTYPING TYPED ALGEBRAS AND COLOURING CYCLIC LINEAR LOGIC

被引：2
|
作者：
Pous, Damien [1 ]
机构：
[1] CNRS, LIG, UMR 5217, Grenoble, France
来源：
LOGICAL METHODS IN COMPUTER SCIENCE | 2012年 / 8卷 / 02期
关键词：
involutive residuated lattices; cyclic linear logic; Kleene algebra; typed algebra; decision procedures; sequent calculus; proof search; KLEENE ALGEBRAS; CALCULUS; SYSTEMS; COQ;
D O I：
10.2168/LMCS-8(2:13)2012
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We prove "untyping" theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped equations. As a consequence, the corresponding untyped decision procedures can be extended for free to the typed settings. Some of these theorems are obtained via a detour through fragments of cyclic linear logic, and give rise to a substantial optimisation of standard proof search algorithms.
引用
收藏
页数：21
相关论文
共 50 条
  • [41] Logic and operator algebras
    Farah, Ilijas
    PROCEEDINGS OF THE INTERNATIONAL CONGRESS OF MATHEMATICIANS (ICM 2014), VOL II, 2014, : 15 - 39
  • [42] Cyclic A∞-algebras and double Poisson algebras
    Fernandez, David
    Herscovich, Estanislao
    JOURNAL OF NONCOMMUTATIVE GEOMETRY, 2021, 15 (01) : 241 - 278
  • [43] Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
    Rouvoet, Arjen
    Poulsen, Casper Bach
    Krebbers, Robbert
    Visser, Eelco
    CPP '20: PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2020, : 284 - 298
  • [44] CONFORMAL ALGEBRAS, VERTEX ALGEBRAS, AND THE LOGIC OF LOCALITY
    Smith, Jonathan D. H.
    MATHEMATICA SLOVACA, 2016, 66 (02) : 407 - 420
  • [45] Typed Meta-interpretive Learning of Logic Programs
    Morel, Rolf
    Cropper, Andrew
    Ong, C. -H. Luke
    LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2019, 2019, 11468 : 198 - 213
  • [46] A Three-Valued Semantics for Typed Logic Programming
    Barbosa, Joao
    Florido, Mario
    Costa, Vitor Santos
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2019, (306): : 36 - 51
  • [47] Coordination of Subject Markers in Arabic and Typed Categorial Logic
    Jebali, Adel
    Biskri, Ismail
    Emirkanian, Louisette
    ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2010, 6085 : 278 - +
  • [48] Proof terms for simply typed higher order logic
    Berghofer, S
    Nipkow, T
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 38 - 52
  • [49] Reuse of results in termination analysis of typed logic programs
    Bruynooghe, M
    Codish, M
    Genaim, S
    Vanhoof, W
    STATIC ANALYSIS, PROCEEDINGS, 2002, 2477 : 477 - 492
  • [50] THE COMPLETION OF TYPED LOGIC PROGRAMS AND SLDNF-RESOLUTION
    HILL, PM
    LOGIC PROGRAMMING AND AUTOMATED REASONING, 1993, 698 : 182 - 193
12345