Penn Arts & Sciences Logo

Logic and Computation Seminar

Wednesday, January 18, 2023 - 3:45pm

Max Kanovich

University College London

Location

University of Pennsylvania

A2 DRL

Contraction rule provided by exponentials is the source of many troubles in linear logic. In particular, to prove undecidability of certain fragments of linear logic, commutative or non-commutative, one uses the whole power of recursive nature of the contraction rule. On the other hand, multiplexing rule has a very clear semantics, namely, !A provides at once any positive number of copies of A. Nevertheless, multiplexing and copying still provide undecidability. With multiplexing, however, there are simple syntactical restrictions that guarantee decidability.