AI 中文总结
该研究探讨推理主义博弈语义，利用类似技术建立基扩展语义（B - eS）与海兰德 - 翁博弈语义的完全抽象关联，并通过4x4数独示例说明语义，为逻辑系统提供了基于证明计算的内涵意义理论。
AI 中文摘要
博弈语义是一种用于推理和计算形式语义的优雅方法，它将模型理论中的真值和有效性概念基于博弈理论概念，强调逻辑推理的动态和交互方面。在海兰德 - 翁博弈中，对局是玩家与环境之间交互的踪迹，此类博弈为源自逻辑系统中证明搜索的计算提供了自然且吸引人的语义。这种语义可被视为从证明（的计算）角度为逻辑系统提供内涵意义理论。在逻辑中，证明论语义，特别是基扩展语义（B - eS）提供了逻辑系统的内涵意义理论，其中在满足关系中原子命题的模型理论解释被使用原子规则‘基’中的可证性的有效性关系所取代。我们利用与桑德奎斯特为直觉主义命题逻辑给出合理且完备的B - eS时所使用的类似技术，建立了B - eS与海兰德 - 翁博弈语义之间的完全抽象关联。我们通过4x4数独示例来说明我们的语义。
英文摘要
Game semantics is an elegant approach to the formal semantics of reasoning and computation that grounds model-theoretic concepts of truth and validity in game-theoretic concepts that emphasize the dynamic and interactive aspects of logical reasoning. In Hyland-Ong games, plays are traces of interactions between a player and an environment and such games provide a naturally appealing semantics for computation that is derived from proof-search in logical systems. Such a semantics can be seen as providing an intensional theory of meaning for systems of logic in terms of (the computation of) proofs. In logic, an intensional theory of meaning for systems of logic is offered by proof-theoretic semantics; in particular, by base-extension semantics (B-eS), in which the model-theoretic interpretation of atomic propositions in a satisfaction relation is replaced by a validity relation which uses provability in `bases' of atomic rules. We establish a fully abstract correlation between B-eS and Hyland-Ong game semantics, employing techniques similar to those used by Sandqvist to give a sound and complete B-eS for intuitionistic propositional logic. We illustrate our semantics through the example of 4x4 Sudoku.
