Linear logic as a logic of computations

34Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the linear implication {multimap}, the tensor product ⊗, and the modal storage operator !. We give a complete computational interpretation for the !-Horn fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known 'or'-like connective ⊕, and, for the sake of the computational duality, we introduce a new 'and'-like connective @ For !-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the (!, ⊕)-Horn fragment of Linear Logic, which uses only positive literals, the linear implication {multimap}, the tensor product ⊗, the modal storage operator!, and the additive 'disjunction' ⊕, we prove that standard Minsky machines [21] can be directly encoded in this (!, ⊕)-Horn fragment. Standard Minsky machines can be directly encoded in the corresponding 'dual' (!, @)-Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable. © 1994.

Cite

CITATION STYLE

APA

Kanovich, M. I. (1994). Linear logic as a logic of computations. Annals of Pure and Applied Logic, 67(1–3), 183–212. https://doi.org/10.1016/0168-0072(94)90011-6

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free