Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Commutative Locative Quantifiers for Multiplicative Linear Logic
verfasst von : Stefano Guerrini, Patrizia Marzuoli
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The paper presents a solution to the technical problem posed by Girard after the introduction of Ludics of how to define proof nets with quantifiers that commute with multiplicatives. According to the principles of Ludics, the commuting quantifiers have a “locative” nature, in particular, quantified formulas are not defined modulo variable renaming. The solution is given by defining a new correctness criterion for first-order multiplicative proof structures that characterizes the system obtained by adding a congruence implying
$\forall{x}(A{\bigotimes}B)=\forall{x}{A}\bigotimes\forall{x}{B}$
to first-order multiplicative linear logic with locative quantifiers. In the conclusions we shall briefly discuss the interpretation of locative quantifiers as storage operators.