Untyping typed algebras and colouring cyclic linear logic

DOI10.2168/LMCS-8(2:13)2012zbMATH Open1241.03009arXiv1205.3612OpenAlexW1985731744MaRDI QIDQ2895474FDOQ2895474

Authors: Damien Pous 

Publication date: 3 July 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1205.3612

Recommendations

• Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic
• Typing theorems of omega algebra
• scientific article; zbMATH DE number 1114352
• scientific article; zbMATH DE number 1231523
• Some Properties of Linear Logic Proved by Semantic Methods

zbMATH Keywords

sequent calculusdecision proceduresKleene algebraproof searchinvolutive residuated latticescyclic linear logictyped algebra

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Other algebras related to logic (03G25)

Cited In (3)

• Typing theorems of omega algebra
• A framework for formal verification of robot kinematics
• Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

Uses Software

• ML
• CASL

This page was built for publication: Untyping typed algebras and colouring cyclic linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2895474)