Linear Logic

Linear logic is a substructural extension to propositional logic.

We have the following operators:

	and	or	true	false
mult	$\otimes$	$⅋$	$1$	$\perp$
add	&	$\oplus$	$\top$	$0$
Multiplicative-Additive Linear Logic

Idea

Multiplicative (grouping)

$\otimes$ (conj) represents the consumption of both resources joinly $⅋$ (disj) represents a dual notion where resources can be split $1$ represents the absence of any resource (neutral element for $\otimes$ ) $\perp$ represents an impossibility.

Additive (choice)

$\&$ represents a choice between resources $\oplus$ represents a choice made by a provider $\top$ is the always true state (neutral for $\&$) $0$ is an impossible choice

Resources

https://www.irif.fr/_media/users/ade/llmgs.pdf Abhishek De and Charles Grellois