187:
Pomset logic was proposed by
Christian Retoré in a semantic formalism with two dual sequential operators existing together with the usual tensor product and par operators of linear logic, the first logic proposed to have both commutative and noncommutative operators. A sequent calculus for the logic
178:
David N. Yetter proposed a weaker structural rule in place of the exchange rule of linear logic, yielding cyclic linear logic. Sequents of cyclic linear logic form a cycle, and so are invariant under rotation, where multipremise rules glue their cycles together at the formulas described in the
136:
on the formulas in sequents. However this is not fully general since some noncommutative logics do not support such an order, such as Yetter's cyclic linear logic. Although most noncommutative logics do not allow weakening or contraction together with noncommutativity, this restriction is not
179:
rules. The calculus supports three structural modalities, a self-dual modality allowing exchange, but still linear, and the usual exponentials (? and !) of linear logic, allowing nonlinear structural rules to be used together with exchange.
211:, which it was argued is necessary for calculi combining commutative and noncommutative operators; this explanation concurs with the difficulty of designing sequent systems for pomset logic that have cut-elimination.
203:
proposed a variation of Retoré's calculus, BV, in which the two noncommutative operations are collapsed onto a single, self-dual, operator, and proposed a novel proof calculus, the
234:, allowing the treatment of more drastically nonstandard logics than those described above, where, for example, the ',' of the sequent calculus is not
214:
Lutz StraĂźburger devised a related system, NEL, also in the calculus of structures in which linear logic with the mix rule appears as a subsystem.
423:
278:
128:
Noncommutative logic is sometimes called ordered logic, since it is possible with most proposed noncommutative logics to impose a
446:
392:
Retoré, Christian (1997-04-02). "Pomset logic: A non-commutative extension of classical linear logic". In
Philippe de Groote;
333:
474:
455:
by
Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré and Eric Villemonte de la Clergerie.
91:
251:
167:
189:
207:
to accommodate the calculus. The principal novelty of the calculus of structures was its pervasive use of
401:
287:
204:
59:
114:
231:
82:
By extension, the term noncommutative logic is also used by a number of authors to refer to a family of
47:
200:
83:
406:
400:. Lecture Notes in Computer Science. Vol. 1210. Springer Berlin Heidelberg. pp. 300–318.
292:
247:
222:
Structads are an approach to the semantics of logic that are based upon generalising the notion of
55:
118:
374:
366:
313:
146:
102:
31:
27:
419:
358:
305:
163:
94:. The remainder of this article is devoted to a presentation of this acceptance of the term.
411:
393:
350:
342:
297:
106:
67:
39:
98:
87:
63:
35:
458:
452:
208:
151:
192:; instead the sense of the calculus was established through a denotational semantics.
468:
256:
133:
378:
442:
110:
71:
43:
20:
459:
Papers on
Commutative/Non-commutative Linear Logic in the calculus of structures
235:
227:
129:
24:
461:: a research homepage from which the papers proposing BV and NEL are available.
354:
415:
362:
309:
51:
331:
Yetter, David N. (1990). "Quantales and (Noncommutative) Linear Logic".
370:
317:
223:
113:
there have been several new noncommutative logics proposed, namely the
166:. His calculus has thus become one of the fundamental formalisms of
159:
346:
301:
276:
Lambek, Joachim (1958). "The
Mathematics of Sentence Structure".
154:
proposed the first noncommutative logic in his 1958 paper
42:
relies on the structure of order varieties (a family of
30:
of linear logic with the noncommutative multiplicative
443:
Non-commutative logic I: the multiplicative fragment
121:of Christian Retoré, and the noncommutative logics
101:, which gave rise to the class of logics known as
158:to model the combinatory possibilities of the
8:
453:Logical aspects of computational linguistics
405:
291:
50:), and the correctness criterion for its
268:
97:The oldest noncommutative logic is the
445:by V. Michele Abrusci and Paul Ruet,
398:Typed Lambda Calculi and Applications
7:
14:
279:The American Mathematical Monthly
156:Mathematics of Sentence Structure
447:Annals of Pure and Applied Logic
122:
1:
334:The Journal of Symbolic Logic
105:. Since the publication of
188:was given, but it lacked a
491:
144:
252:substructural type system
168:computational linguistics
78:Noncommutativity in logic
416:10.1007/3-540-62688-3_43
46:that may be viewed as a
190:cut-elimination theorem
205:calculus of structures
60:denotational semantics
232:combinatorial species
117:of David Yetter, the
54:is given in terms of
84:substructural logics
56:partial permutations
48:species of structure
17:Noncommutative logic
475:Substructural logic
248:Ordered type system
226:along the lines of
174:Cyclic linear logic
141:The Lambek calculus
115:cyclic linear logic
103:categorial grammars
70:over some specific
66:are interpreted by
19:is an extension of
355:10338.dmlcz/140417
147:categorial grammar
23:that combines the
425:978-3-540-62688-6
201:Alessio Guglielmi
164:natural languages
482:
430:
429:
409:
394:J. Roger Hindley
389:
383:
382:
328:
322:
321:
295:
273:
107:Jean-Yves Girard
58:. It also has a
40:sequent calculus
490:
489:
485:
484:
483:
481:
480:
479:
465:
464:
439:
434:
433:
426:
391:
390:
386:
347:10.2307/2274953
330:
329:
325:
302:10.2307/2310058
275:
274:
270:
265:
244:
220:
198:
185:
176:
149:
143:
99:Lambek calculus
80:
36:Lambek calculus
12:
11:
5:
488:
486:
478:
477:
467:
466:
463:
462:
456:
450:
438:
437:External links
435:
432:
431:
424:
407:10.1.1.47.2354
384:
323:
293:10.1.1.538.885
286:(3): 154–170.
267:
266:
264:
261:
260:
259:
254:
243:
240:
219:
216:
209:deep inference
197:
194:
184:
181:
175:
172:
152:Joachim Lambek
145:Main article:
142:
139:
79:
76:
13:
10:
9:
6:
4:
3:
2:
487:
476:
473:
472:
470:
460:
457:
454:
451:
449:101(1), 2000.
448:
444:
441:
440:
436:
427:
421:
417:
413:
408:
403:
399:
395:
388:
385:
380:
376:
372:
368:
364:
360:
356:
352:
348:
344:
340:
336:
335:
327:
324:
319:
315:
311:
307:
303:
299:
294:
289:
285:
281:
280:
272:
269:
262:
258:
257:Quantum logic
255:
253:
249:
246:
245:
241:
239:
237:
233:
229:
225:
217:
215:
212:
210:
206:
202:
195:
193:
191:
182:
180:
173:
171:
169:
165:
161:
157:
153:
148:
140:
138:
135:
134:partial order
131:
126:
124:
120:
116:
112:
108:
104:
100:
95:
93:
89:
88:exchange rule
86:in which the
85:
77:
75:
73:
72:Hopf algebras
69:
65:
61:
57:
53:
49:
45:
44:cyclic orders
41:
37:
33:
29:
26:
22:
18:
397:
387:
341:(1): 41–64.
338:
332:
326:
283:
277:
271:
221:
213:
199:
186:
183:Pomset logic
177:
155:
150:
127:
119:pomset logic
111:linear logic
96:
92:inadmissible
81:
21:linear logic
16:
15:
236:associative
137:necessary.
32:connectives
28:connectives
25:commutative
263:References
196:BV and NEL
123:BV and NEL
52:proof nets
402:CiteSeerX
363:0022-4812
310:0002-9890
288:CiteSeerX
218:Structads
62:in which
469:Category
396:(eds.).
379:30626492
242:See also
64:formulas
371:2274953
318:2310058
224:sequent
68:modules
34:of the
422:
404:
377:
369:
361:
316:
308:
290:
160:syntax
38:. Its
375:S2CID
367:JSTOR
314:JSTOR
228:Joyal
130:total
420:ISBN
359:ISSN
306:ISSN
250:, a
412:doi
351:hdl
343:doi
298:doi
230:'s
162:of
132:or
109:'s
90:is
471::
418:.
410:.
373:.
365:.
357:.
349:.
339:55
337:.
312:.
304:.
296:.
284:65
282:.
238:.
170:.
125:.
74:.
428:.
414::
381:.
353::
345::
320:.
300::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.