Stellar Resolution: Multiplicatives - for the linear logician, through examples
Résumé
The stellar resolution is an asynchronous model of computation used in Girard's Transcendental Syntax which is based of Robinson's resolution. Similarly to classical realisability, we obtain a new model of linear logic with computational objects as its foundation: proofs, cut-elimination, formulas/types, correctness and provability are reconstructed very naturally. In this paper, we investigate the case of the multiplicative fragment of linear logic.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...