DocumentCode
2717094
Title
Normal process representatives
Author
Gehlot, Vijay ; Gunter, Carl
Author_Institution
Dept. of Comput. & Inf. Sci., Pennsylvania Univ., Philadelphia, PA, USA
fYear
1990
fDate
4-7 Jun 1990
Firstpage
200
Lastpage
207
Abstract
The relevance of a form of cut elimination theorem for linear logic tensor theories to the concept of a process on a Petri net is discussed. The discussion is based on two definitions of processes given by E. Best and R. Devillers (1987). 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 finer of these definitions. Using a strongly normalizing rewrite system and a weak Church-Rosser theorem, it is shown that each class of the coarser process definition contains exactly one of these finer classes which can therefore be viewed as a canonical or normal process representative. The relevance of these rewrite rules to the categorical approach of P. Degano et al. (1989) is also discussed
Keywords
Petri nets; formal logic; rewriting systems; theorem proving; Petri net; canonical; coarser process definition; cut elimination theorem; cut reduced proofs; equivalence relations; linear logic tensor theories; normal process representation; strongly normalizing rewrite system; weak Church-Rosser theorem;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Conference_Location
Philadelphia, PA
Print_ISBN
0-8186-2073-0
Type
conf
DOI
10.1109/LICS.1990.113746
Filename
113746
Link To Document