Ugo Dal Lago and Simone Martini. Phase semantics and decidability of elementary affine logic. Theoretical Computer Science, 2004. To appear.

Light, elementary and soft linear logics are formal systems derived from Linear Logic, enjoying remarkable normalization properties. In this paper we prove decidability of Elementary A ne Logic, EAL. The result is obtained by semantical means, first defining a class of phase models for EAL and then proving soundness and (strong) completeness, following Okada s technique. Phase models for Light A ne Logic and Soft Linear Logic are also defined and shown complete.

[ bib | http ]

Back