Multiplicative Additive Linear Logic

Multiplicative Additive Linear Logic (MALL) is the fragment of linear logic consisting of

• the multiplicative connectives \otimes and ⅋
• the additive connectives & and \oplus
• (optionally) their units

Because of the presence of ⅋, MLL is a fragment of classical linear logic.

Proof nets

Please expand.

Models

Abramsky-Melliès concurrent games are fully complete for MALL Abramsky and Melliès 1999.

Decidability

Please expand.

See also

• Linear Logic
• Multiplicative Exponential Linear Logic

References

@inproceedings{abramsky_1999,
	title = {Concurrent games and full completeness},
	doi = {10.1109/LICS.1999.782638},
	booktitle = {Proceedings. 14th {Symposium} on {Logic} in {Computer} {Science} ({Cat}. {No}. {PR00158})},
	publisher = {IEEE Computer Society},
	author = {Abramsky, S. and Melli\`{e}s, P.-A.},
	year = {1999},
	pages = {431--442}
}