Various kinds of game semantics have been introduced to characterize computational features of substructural logics, in particular fragments and variants of linear logic (LL) [5]. This line of research can be traced back to Lorenzen’s dialogues for intuitionistic logic [6] and to the works of Blass [2,3], Abramsky and Jagadeesan [1], among several others.

We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game for affine intuitionistic linear logic, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by using subexponentials ([4][7]) for representing two types of options - volatile and permanent - for purchasing resources. This leads to a new type of subexponential calculus where costs are attached to sequents. Different proofs are interpreted as more or less expensive strategies to obtain a certain resource from a bunch of resources (priced options). We also generalize the concept of costs and option’s prices in proofs by using a semiring structure. This allows for the interpretation a wider range of subexponential systems, giving meaning to resources in proofs in a more flexible way. We conclude by studying some proof-theoretical properties of the proposed systems, justifying our intended meaning for costs and resources.

[1] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Log., 59(2):543–574, 1994.

[2] Andreas Blass. A game semantics for linear logic. Ann. Pure Appl. Logic, 56(1-3):183–220,1992.

[3] Andreas Blass. Some semantical aspects of linear logic. Logic Journal of the IGPL, 5(4):487–503, 1997.

[4] Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Kurt Gödel Colloquium, volume 713 of Lecture Notes in Computer Science, pages 159–171. Springer, 1993.

[5] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987.

[6] Paul Lorenzen. Logik und agon. Atti Del XII Congresso Internazionale di Filosofia, 4:187–194, 1960.

[7] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, PPDP, pages 129–140. ACM,2009.