Multi-Agent Dialogues and Dialogue Sequents for Proof Search and Scheduling in Intuitionistic Logic and the Modal Logic S4

摘要

Dialogical games as introduced by Lorenzen and Lorenz describe a reasoning technique for intuitionistic and classical predicate logic: two players (proponent and opponent) argue about the validity of a given formula according to predefined rules. If the proponent has a winning strategy then the formula is proven to be valid. The underlying game rules can be modified to have an impact on proof search strategies and increase the efficiency of such a searching process. In this paper, a multi-agent version of dialogical logic is introduced that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones which are more related to two-player dialogues. We also consider an extension for the normal modal logic S4. The rules lead us to a normalization of a proof, let us focus on the proponents' relevant decisions, and therefore give explicit directives that increase compactness of the proofsearching process. This allows us to perform parts of the proof in a parallel way. We prove soundness and completeness of these multi-agent systems.