DocumentCode
299482
Title
Games semantics for full propositional linear logic
Author
Lamarche, Francois
Author_Institution
Dept. of Comput., Imperial Coll. of Sci., Technol. & Med., London, UK
fYear
1995
fDate
26-29 Jun 1995
Firstpage
464
Lastpage
473
Abstract
We present a model of propositional classical linear logic (all the connective except for the additive constants) where the formulas are seen as two person games in which connectives are used as tokens, while the proofs are interpreted as strategies for one player. We discuss the intimate connection between these games and the structure of proofs, and prove a full completeness theorem. The main technical innovation is a “double negation” interpretation of CLL into intuitionistic linear logic
Keywords
formal logic; game theory; CLL; CLL interpretation; connectives; double negation; full completeness theorem; full propositional linear logic; games semantics; intuitionistic linear logic; proofs; propositional classical linear logic; technical innovation; two person games; Concrete; Context modeling; Data structures; Ear; Educational institutions; Game theory; IEEE news; Logic; Technological innovation;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location
San Diego, CA
ISSN
1043-6871
Print_ISBN
0-8186-7050-9
Type
conf
DOI
10.1109/LICS.1995.523280
Filename
523280
Link To Document