[Prev][Next][Index][Thread]
Mix Rule and Girardian Turnstile
One request and one question:
1. The request is for the "official" LaTeX macro for the Girardian turnstile.
2. The question is about the MIX rule
/- A /- B
---------------
/- A par B
that Girard mentions. What are the consequences of having such
a rule (other than A tensor B -o A par B)? Has anyone used
the MIX rule to explain parallel composition of process calculi such
as CCS, particularly the way the parallel composition operator
(CCS |) is used to represent both connected and unconnected concurrency?
How would the MIX rule be rendered in LU? Am I right in
conjecturing the following?
; Gamma' /- Delta' ; A ; Gamma' /- Delta' ; B
------------------------------------------------------
; Gamma' /- Delta' ; A par B
Thanks in advance for any insights.
- Sanjiva (sanjiva@ecrc.de)
PS: I'm quite new to linear logic, and I'm interested more in
proof assignment than in proof search.