Normal Process Representatives

This paper discusses the relevance of a form of cut elimination theorem for linear logic tensor theories to the concept of a process on a Petri net. We base our discussion on two denitions of processes given by Best and Devillers. Their notions of process correspond to equivalence relations on linear logic proofs. It is noted that the cut reduced proofs form a process under the ner of these denitions. Using a strongly normalizing rewrite system and a weak Church-Rosser theorem, we show that each class of the coarser process denition contains exactly one of these ner classes which can therefore be viewed as a canonical or normal process representative. We also discuss the relevance of our rewrite rules to the categorical approach of Degano, Meseguer, and Montanari.

• Type: Conference
• Year: 1990
• Where: LICS
• Authors: Vijay Gehlot, Carl A. Gunter
• Keywords: Automated Reasoning, Cut Elimination Theorem, LICS 1990, Linear Logic, Linear Logic Tensor