Building Tableaux for Intuitionistic Linear Logic

• Hugo Hoffmann Borges PUC-Rio

DOI: https://doi.org/10.5753/wbl.2022.222837

Abstract

The purpose of this article is to build a sound and complete Tableaux for Intuitionist Linear Logic through a process of translating the Sequent Calculus rules.

Keywords: Proof Theory, Tableaux, Linear Logic, Intuitionistic Linear Logic

References

Fitting, M. (1999). General introduction. In M. D‘Agostino, D. G. and Hähnle, R., editors, Handbook of Tableau Methods. Springer.

M. D‘Agostino, D. G. and Broda, K. (1999). Tableau methods for substructural logic. In M. D‘Agostino, D. G. and Hähnle, R., editors, Handbook of Tableau Methods. Springer.

Mantel, H. and Otten, J. (1999). lintap: A tableau prover for linear logic. In TABLEAUX.

Okada, M. (1998). Introduction to linear logic: Expressiveness and phase semantics. In M. Dezani-Ciancaglini, M. O. and Takahashi, M., editors, Mathematical Society of Japan Memories vol.2.

R. Meyer, M. M. and Belnap, N. (1995). Linear analytic tableaux. In P. Baumgarten, R. H. and Possega, J., editors, Theorem Proving with Analytic Tableaux and Related Methods. Springer.