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