CMU-CS-01-129
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-01-129
Fixpoint Semantics for a Fragment of First-Order Linear Logic
Marco Bozzano*
May 2001
CMU-CS-01-129.ps
CMU-CS-01-129.pdf
Keywords: Linear logic, fixpoint semantics
In this paper we investigate the theoretical foundation of a
bottom-up, fixpoint semantics for a subset of Girard's linear
logic. More precisely, we consider a first-order formulation of a fragment
of LinLog including multiplicative disjunction and
universal quantification over goals. The semantics is defined by
means of a fixpoint operator which is monotonic and continuous over
an extended notion of interpretation lattice. We prove soundness and
completeness of this semantics with respect to the usual operational
semantics. We discuss some applications and related work.
22 pages
*DISI, Universita di Genova, Italy
|