Untyping typed algebras and colouring cyclic linear logic

DOI10.2168/LMCS-8(2:13)2012MaRDI QIDQ2895474zbMATHOpenAlexFDO

Authors Damien Pous

Publication date 3 July 2012

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

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

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)

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.

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

Cited in

(3)

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

Describes a project that uses

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)