论文标题
建设性的游戏逻辑
Constructive Game Logic
论文作者
论文摘要
游戏逻辑是通过将这些证明作为程序解释来研究证明的绝佳环境，因为游戏的建设性证明与有效的获胜策略相对应，以响应对手的行为。因此，我们开发了建设性的游戏逻辑，该游戏逻辑扩展了Parikh的游戏逻辑（GL），并使用一阶程序A La Pratt的一阶动力学逻辑（DL）。我们的主要贡献包括： 1）一种新型的可实现性语义捕获游戏的对抗动力学，2）自然扣除微积分和操作语义，通过证明来描述策略的计算含义，以及3）理论结果，包括证明计算W.R.T.的声音。可靠性语义，对证明的操作语义的进度和保存以及支持从游戏证明中提取计算文物的存在。 总之，这些结果为迄今为止的任何程序逻辑提供了咖喱途径解释的最一般性说明，也是游戏逻辑的第一个逻辑。
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's actions. We thus develop Constructive Game Logic which extends Parikh's Game Logic (GL) with constructivity and with first-order programs a la Pratt's first-order dynamic logic (DL). Our major contributions include: 1) a novel realizability semantics capturing the adversarial dynamics of games, 2) a natural deduction calculus and operational semantics describing the computational meaning of strategies via proof-terms, and 3) theoretical results including soundness of the proof calculus w.r.t. realizability semantics, progress and preservation of the operational semantics of proofs, and Existence Properties on support of the extraction of computational artifacts from game proofs. Together, these results provide the most general account of a Curry-Howard interpretation for any program logic to date, and the first at all for Game Logic.
