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 Affine 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 Affine Logic and Soft Linear Logic are also defined and shown complete.
Phase Semantics and Decidability of Elementary Affine Logic / MARTINI S.; DAL LAGO U.. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - STAMPA. - 318(3):(2004), pp. 409-433. [10.1016/j.tcs.2004.02.037]
Phase Semantics and Decidability of Elementary Affine Logic
MARTINI, SIMONE;DAL LAGO, UGO
2004
Abstract
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 Affine 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 Affine Logic and Soft Linear Logic are also defined and shown complete.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
