Linear logic with fixed resources
type: Item
instance of: scholarly article
title: Linear logic with fixed resources
zbMATH Open document ID: 0813.03010
DOI: 10.1016/0168-0072(94)90006-X
author: Michael A. Taitslin
author: Dmitri A. Archangelsky
published in: Annals of Pure and Applied Logic
publication date: 1995-06-08T00:00:00Z
review text: This paper aims at providing a variant of linear logic with modalities, for which a non-exponential algorithm checks provability and provides a proof for a given sequent. This contrasts with NP-completeness of this problem for the Horn fragment of linear logic. Linearity is understood as a control on availability of two sorts of supplies: variables and `convertors', that is, linear implications between conjunctions of variables. This is specified at each node of a fixed net of communication, having the form of a tree. Availability of modalities is treated in a way similar to Kripke models. This models to define truth of a sequent of a node; but also to elaborate a proof system with axioms attached to available supplies. Using a rather technical reduction to `canonical proofs', soundness and completeness are proven. Finally, the authors provide the announced algorithm.
reviewed by: N. Bernard
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 584679
zbMATH Keywords: proof theory
zbMATH Keywords: models
zbMATH Keywords: nonexponential algorithm checking provability and providing a proof
zbMATH Keywords: linear logic with modalities
zbMATH Keywords: provability
zbMATH Keywords: sequent
zbMATH Keywords: net of communication
MaRDI profile type: Publication
cites work: Linear logic
cites work: The linear abstract machine
full work available at URL: 0168-0072(94)90006-x
OpenAlex ID: W2016867439
description: scientific article; zbMATH DE number 584679