First-Order Dialogical Games and Tableaux
Nicolas Clerbout
Maison de la Recherche, salle 008.
Résumé :
This talk has two purposes. The first one is to present a formulation of first-order dialogical logic where the (structural) rules are formulated in termes of repetition ranks. In particular, I will answer to the question I mentioned in a previous talk about the distinction between Classical and Intuitionistic dialogical games when formulated with repetition ranks. Furthermore, I will (briefly) present extensive forms of games and of strategies.
The second and main purpose of the talk is to study the connection between dialogical games and tableaux. The point is to prove the following theorem for Classical Logic:
There is a winning P strategy in the dialogical game for a formula if, and only if, there is a tableau proof for that formula.
As for the proof of this theorem, I will present the main features of the proof of the "left-to-right" direction (that is, from to strategies to tableaux proofs) and the state of the art for the proof of the "right-to-left" direction.
