[Back]

J. Alama:
"New views into dialogue games for classical and intuitionistic logic";
Talk: Seminar Faculty of Information Systems and Applied Computer Science @ University of Bamberg, Bamberg, Germany (invited); 2014-12-16.

Dialogue games ("dialogues" for short) are a two-player game semantics for a variety of logics. Proponent makes an initial claim, and Opponent disputes this; the players take turns attacking and defending claims until one of the players loses. The logical significance of dialogues appears at the level of winning strategies: we are interested in whether it is possible for Proponent to play in such a way that he can successfully reply to any potential Opponent move. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. In our experience, the rules of dialogue games, though intuitively attractive, can be subtle; playing the games by hand can easily lead to mistakes. Implementing dialogues can help to rule out these kinds of errors. More importantly, an implementation can go beyond simply "keeping us honest" as we play the game, but give new insights into dialogues that might not be easily seen without computer assistance.

We present a theoretical result that has come out of our research tool: a characterization of dialogue games for classical logic in which the so-called E rule (which says that the Opponent must immediately respond to whatever Proponent said in the previous move) is relaxed. We also present an experimental theorem prover for intuitionistic first-order logic whose underlying calculus is based on dialogue games. One finds, again, that our understanding of dialogue games is improved by seeing how the game-based theorem prover performs on non-trivial theorem-proving problems.