We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
The completeness of linear logic for Petri net models.
- Authors
Ishihara, K; Hiraishi, K
- Abstract
The completeness between linear logic and Petri nets has been shown for several versions of linear logic. For example, Engberg and Winskel considered the [sqcup ]-free fragment of propositional intuitionistic linear logic without exponential ¡, and showed soundness and completeness of the logic for a Petri net model. One of difficulties in proving completeness for full propositional intuitionalistic linear logic lies in distributivity of [sqcap ] over [sqcup ], that is not valid in linear logic. The quantales constructed by Engberg and Winskel are distributive lattices, i.e., distributivity is always valid. In this paper, we first construct non-distributive quantales from Petri nets by using a closure operation, and prove completeness of full linear logic without exponential for them. Next we extend the construction of the quantales to those with exponential ¡, and prove completeness of linear logic with exponential for the quantales. We also give an impression on the meaning of the logic on the proposed Petri net model, comparing with that by Engberg and Winskel.
- Subjects
LOGIC; PETRI nets; INTUITIONISTIC mathematics; DISTRIBUTION (Probability theory); LATTICE theory
- Publication
Logic Journal of the IGPL, 2001, Vol 9, Issue 4, p549
- ISSN
1367-0751
- Publication type
Article
- DOI
10.1093/jigpal/9.4.549