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 条
  • [31] v*-ALGEBRAS, INDEPENDENCE ALGEBRAS AND LOGIC
    Araujo, Joao
    Edmundo, Mario
    Givant, Steven
    INTERNATIONAL JOURNAL OF ALGEBRA AND COMPUTATION, 2011, 21 (07) : 1237 - 1257
  • [32] On cyclic algebras
    Albert, AA
    ANNALS OF MATHEMATICS, 1938, 39 : 669 - 682
  • [33] Rough algebras and fuzzy logic algebras
    Zhang, Xiao-hong
    FOURTH INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS AND KNOWLEDGE DISCOVERY, VOL 1, PROCEEDINGS, 2007, : 213 - 216
  • [34] CYCLIC A∞-ALGEBRAS AND CYCLIC HOMOLOGY
    Herscovich, Estanislao
    HOMOLOGY HOMOTOPY AND APPLICATIONS, 2023, 25 (01) : 287 - 318
  • [35] Linear colouring of binomial random graphs
    Eide, Austin
    Pralat, Pawel
    DISCRETE MATHEMATICS, 2025, 348 (02)
  • [36] A correspondence between maximal abelian sub-algebras and linear logic fragments
    Seiller, Thomas
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2018, 28 (01) : 77 - 139
  • [37] Cyclic Multiplicative Proof Nets of Linear Logic with an Application to Language Parsing
    Abrusci, Vito Michele
    Maieli, Roberto
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2015, 2015, 9160 : 53 - 68
  • [38] Cyclic reference counting by typed reference fields
    Chang, J. Morris
    Chen, Wei-Mei
    Griffin, Paul A.
    Cheng, Ho-Yuan
    COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2012, 38 (01) : 98 - 107
  • [39] Typed event structures and the linear π-calculus
    Varacca, Daniele
    Yoshida, Nobuko
    THEORETICAL COMPUTER SCIENCE, 2010, 411 (19) : 1949 - 1973
  • [40] On amalgamation in algebras of logic
    Ahmed T.S.
    Studia Logica, 2005, 81 (1) : 61 - 77
12345