Title :
Decidability of linear affine logic
Author_Institution :
Dept. of Math. & Mech., Moscow State Univ.
Abstract :
The propositional linear logic is known to be undecidable. We prove that the full propositional linear affine logic containing all multiplicatives, additives, exponentials, and constants is decidable. The proof is based on a reduction of linear affine logic to sequents of specific “normal forms”, and on a generalization of M.I. Kanovich´s (1992) computational interpretation of linear logic adaptive to these “normal forms”
Keywords :
decidability; formal logic; programming theory; Kanovich computational interpretation; linear affine logic; multiplicatives; normal forms; propositional linear affine logic; undecidable; Logic;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523283