README⤓ .txt 2026-10-22T165042.936 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-08-20T092124.000 000000000034904 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-08-20T103407.000 000000000041176 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-10-22T180154.561 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-10-22T165042.936 000000000000816 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-08-20T093823.000 000000000034872 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-08-20T094438.000 000000000033864 Lorenzen, Lorenz (1960s). Erlangen school. Game semantics. Dialogue games. Foundation of constructive semantics.
Dynamic Logic⤓ .md 2026-08-20T083225.000 000000000044784 Vaughan Pratt introduced dynamic logic in 1976 ("Semantical considerations on Floyd–Hoare logic"), reading programs as modalities. Fischer and Ladner isolated the propositional fragment PDL, combining modal logic with regular expressions over programs, and settled its complexity (1977, 1979). David Harel developed the first-order theory (1979). Foundational for program verification and reasoning about actions.
Ehrenfeucht-Fraisse Games⤓ .md 2026-08-20T025129.000 000000000041592 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-08-20T095134.000 000000000032544 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-08-20T075111.000 000000000040168 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-10-22T165042.936 000000000000808 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-10-22T090048.000 000000000039240 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-10-22T092853.000 000000000037168 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-08-20T030722.000 000000000049264 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-08-20T074348.000 000000000038552 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-08-20T100548.000 000000000033432 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-08-20T103725.000 000000000034312 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-10-22T090052.000 000000000039616 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-15T162259.000 000000000007288 Not sufficient: A logic that merely admits a game-theoretic model without games as its content. A probabilistic decision framework (Probabilistic).