Affiliations: Informatics Theory Group, University of Bamberg, Germany. [email protected]
Correspondence:
[†]
Address for correspondence: Informatics Theory Group, University of Bamberg, Kapuzinerstrasse 16, D-96047 Bamberg, Germany
Note: [*] partially funded by Austrian Science Fund (FWF) project P25417-G15 (LOGFRADIG)
Abstract: 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 multi-conclusion 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.
