Authors: Damien Pous

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.

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