• README ⤓ .txt 2026-07-17T121634.146 000000000000752
  Logics whose semantics or subject matter is strategic interaction: systems in which truth, provability, or meaning is cast as the existence of a winning strategy, and logics for reasoning about games, strategies, and coalitions. Games serve here both as a semantic tool and as an object of formal theory.
• Banach-Mazur Games ⤓ .md 2026-07-15T071433.000 000000000013784
  Banach and Mazur (1930s), Oxtoby (1957). Infinite games on topological spaces. Players choose nested sets. Winning = nonempty intersection. Foundation for descriptive set theory.
• Borel Determinacy ⤓ .md 2026-07-15T072158.000 000000000015464
  Martin (1975). Infinite games with Borel winning sets are determined. One player has winning strategy. Beyond Borel: requires large cardinals. Foundation for descriptive set theory.
• Buchi Automata ⤓ .md 2026-07-17T120407.600 000000000000872
  J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.
• Coalition Logic ⤓ .md 2026-07-15T054810.000 000000000026368
  Marc Pauly developed coalition logic (2000, 2002). Extends modal logic to reason about what groups of agents can achieve. Alternating-time Temporal Logic (ATL) by Alur, Henzinger, and Kupferman (1997, 2002) combines coalition power with temporal logic. Foundation for multi-agent system verification.
• Concurrent Game Logic ⤓ .md 2026-07-15T060304.000 000000000021392
  Alur, Henzinger, and Kupferman introduced concurrent game structures (1997-2002). Agents act simultaneously rather than taking turns. Generalizes turn-based games to concurrent moves. ATL and ATL* designed for this setting. Models reactive systems with simultaneous interaction.
• Dialogical Logic ⤓ .md 2026-07-17T120407.600 000000000000824
  Lorenzen, Lorenz (1960s). Erlangen school. Game semantics. Dialogue games. Foundation of constructive semantics.
• Dynamic Logic ⤓ .md 2026-07-15T052745.000 000000000026680
  Vaughan Pratt introduced Propositional Dynamic Logic (PDL) in 1976, combining modal logic with regular expressions over programs. David Harel extended it to first-order (1979). Fischer and Ladner analyzed complexity. Foundational for program verification and reasoning about actions.
• Ehrenfeucht-Fraisse Games ⤓ .md 2026-07-15T065144.000 000000000015216
  Ehrenfeucht (1961) building on Fraïssé (1954). Game characterization of elementary equivalence. Spoiler vs Duplicator. n-round game captures n-quantifier equivalence.
• Extensive Game Logic ⤓ .md 2026-07-15T235628.000 000000000019232
  Bonanno's modal logic of extensive games (2001, 2002); Harrenstein, van der Hoek, Meyer, and Witteveen on game-theoretic reasoning in modal logic (2002, 2003); van Benthem's "Games in dynamic-epistemic logic" (2001) and Logic in Games (2014). Logic for extensive form games. Tree-structured games with perfect/imperfect information. Epistemic reasoning about game positions. Backward induction, subgame perfection.
• Game Logic ⤓ .md 2026-07-15T054808.000 000000000025352
  Rohit Parikh introduced propositional game logic (1985). Builds on dynamic logic, adding game-theoretic operations. Models strategic interaction where outcomes depend on choices of multiple agents. Connects logic, game theory, and verification. Extended by various researchers for different game-theoretic concepts.
• Game Semantics ⤓ .md 2026-07-15T061325.000 000000000020848
  Lorenzen's dialogical logic (1960s). Hintikka's game-theoretic semantics (1970s). Abramsky, Jagadeesan, Malacaria: full abstraction (1990s). Games between Proponent (verifier) and Opponent (falsifier). Foundation for programming language semantics.
• Ludics ⤓ .md 2026-07-15T063259.000 000000000017992
  Girard introduced ludics (2001). Foundation for logic via interactive games. Designs as basic objects, not formulas. Orthogonality defines behavior/type. Unifies logic, computation, and game semantics. "Logic from interaction."
• Mechanism Design Logic ⤓ .md 2026-07-15T063454.000 000000000019600
  Connects mechanism design (Hurwicz, 1960s) to logic. Pauly's coalition logic. Van der Hoek, Wooldridge: social choice in logic. Formal verification of mechanisms. Automated mechanism design foundations.
• Modal Mu-Calculus ⤓ .md 2026-07-17T120407.600 000000000000848
  Dana Scott and Jaco de Bakker used fixed points in program semantics (1969); Park (1969, 1976) on fixpoint induction. Dexter Kozen, "Results on the propositional μ-calculus" (1983), gave the system and its axiomatization; Walukiewicz (1995) proved completeness. The modal mu-calculus combines modal logic with fixed-point operators. Subsumes CTL, LTL, PDL in expressive power. Foundation for model checking algorithms (OBDD-based, game-based).
• Parity Games ⤓ .md 2026-07-15T065146.000 000000000015248
  Emerson and Jutla (1991). Two-player infinite games on graphs. Parity condition on infinite plays. Decides μ-calculus satisfiability. Positional strategies suffice.
• Sabotage Game Logic ⤓ .md 2026-07-15T061942.000 000000000017784
  Extends sabotage logic to full game-theoretic setting. Van Benthem's sabotage games (2002). Combines sabotage with game logic and ATL-style reasoning. Multi-agent adversarial graph modification. Strategic reasoning under sabotage.
• Signaling Game Logic ⤓ .md 2026-07-15T062737.000 000000000018344
  Lewis's signaling games (1969). Spence's signaling (economics, 1973). Game-theoretic semantics of communication. Logic for strategic information transmission. Foundation for pragmatics and mechanism design.
• Strategy Logic ⤓ .md 2026-07-15T055419.000 000000000025216
  Krishnendu Chatterjee, Thomas Henzinger, and Nir Piterman introduced Strategy Logic (SL, 2007, 2010). Extends ATL with explicit strategy quantification. Strategies are first-class objects: quantify over them, bind them to agents. More expressive than ATL* but with higher complexity. Foundation for advanced multi-agent verification.
• CRITERIA ⤓ .txt 2026-07-17T120407.600 000000000000768
  Not sufficient: A logic that merely admits a game-theoretic model without games as its content. A probabilistic decision framework (Probabilistic).