Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

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.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Damien Pous
• Keywords: Automated Reasoning, Corresponding Untyped Decision, CSL 2010, Involutive Residuated Lattices, Untyped Equations