Editing Game semantics (section)

==History==
In the late 1950s [[Paul Lorenzen]] was the first to introduce a game semantics for [[logic]], and it was further developed by [[Kuno Lorenz]]. At almost the same time as Lorenzen, [[Jaakko Hintikka]] developed a [[model theory|model-theoretical]] approach known in the literature as ''GTS'' (game-theoretical semantics). Since then, a number of different game semantics have been studied in logic.

Shahid Rahman ([[Charles de Gaulle University – Lille III|Lille III]]) and collaborators developed [[dialogical logic]] into a general framework for the study of logical and philosophical issues related to [[logical pluralism]]. Beginning 1994 this triggered a kind of renaissance with lasting consequences. This new philosophical impulse experienced a parallel renewal in the fields of [[theoretical computer science]], [[computational linguistics]], [[artificial intelligence]], and the [[formal semantics of programming languages]], for instance the work of [[Johan van Benthem (logician)|Johan van Benthem]] and collaborators in [[Amsterdam]] who looked thoroughly at the interface between logic and games, and Hanno Nickau who addressed the full abstraction problem in programming languages by means of games. New results in [[linear logic]] by [[Jean-Yves Girard]] in the interfaces between mathematical game theory and [[logic]] on one hand and [[argumentation theory]] and logic on the other hand resulted in the work of many others, including [[Samson Abramsky|S. Abramsky]], J. van Benthem, [[Andreas Blass|A. Blass]], [[Dov Gabbay|D. Gabbay]], [[Martin Hyland|M. Hyland]], [[Wilfred Hodges|W. Hodges]], R. Jagadeesan, [[Giorgi Japaridze|G. Japaridze]], E. Krabbe, L. Ong, H. Prakken, G. Sandu, D. Walton, and J. Woods, who placed game semantics at the center of a new concept in logic in which logic is understood as a dynamic instrument of inference. There has also been an alternative perspective on [[proof theory]] and meaning theory, advocating that [[Wittgenstein]]'s "meaning as use" paradigm as understood in the context of proof theory, where the so-called reduction rules (showing the effect of elimination rules on the result of introduction rules) should be seen as appropriate to formalise the explanation of the (immediate) consequences one can draw from a proposition, thus showing the function/purpose/usefulness of its main connective in the calculus of language ({{harvtxt|de Queiroz|1988}}, {{harvtxt|de Queiroz|1991}}, {{harvtxt|de Queiroz|1994}}, {{harvtxt|de Queiroz|2001}}, {{harvtxt|de Queiroz|2008}}, {{harvtxt|de Queiroz|2023}}).