LLW is decidable

• To: linear@cs.stanford.edu
• Subject: LLW is decidable
• From: artemov@fwi.uva.nl (Sergei Artemov )
• Date: Thu, 13 Oct 1994 19:40:37 +0100
• Approved: types@dcs.gla.ac.uk

The paper by A.Kopylov 
 
\title{Decidability of Linear Affine Logic}
\author{Alexei P. Kopylov \\
Department of Mathematics and Mechanics \\
Moscow State University \\
119899, Moscow, Russia}
\date{September, 1994} 
 
\begin{abstract}
The propositional Linear Logic is known to be undecidable.
In the current paper we prove that the full propositional Linear Affine
Logic containing all the multiplicatives, additives, exponentials,
and constants is decidable. The proof is based on a
reduction of the Linear Affine Logic to sequents of
specific ``normal forms'', and
on vector games interpretation adapted to these ``normal forms''.
\end{abstract}

is now issued as the preprint

 CNRS, Laboratoire de Math\'{e}matiques Discr\`{e}tes,
 Pr\'{e}tirage n$^\circ$ 94-32, ~1994, 30~p.\\
 Available by anonymous ftp from host lmd.univ-mrs.fr
 and the file pub/kopylov/fin.dvi

Best regards, 
Sergei Artemov  

• Prev: LLL
• Next: DIMACS Special Year on Logic and Complexity
• Index(es):
  • Main
  • Thread