Proof search in multi-agent dialogues for modal logic

In computer science, modal logics play an important role in various areas, e. g., to model knowledge structures or ontologies. Intuitionistic or constructive propositional logic can be considered as a special kind of modal logic. Constructive modal logics describe a restrictive family of modal systems. To prove validity of a statement formalized in such logics, various reasoning procedures (calculi) have been investigated. When searching for proofs, a normalization of deductions in a calculus is desired. A new attempt to find a normalized calculus leads to dialogical logic, a game-theoretic reasoning technique. Usually, two players, one proponent and one opponent, argue about an assertion, expressed as a formula and stated by the proponent at the beginning of the play. The dialogical approach is very flexible as the game rules can be adjusted easily. It turns out that intro-ducing further proponent-players who fight one opponent in a round-based setting leads to a normalization of proofs. Ordinary sequent systems can easily be transferred into the dialectic setting to achieve that normalization. Further, the round-based scheduling induces a method to parallelize the reasoning process. Modifying the game rules makes it possible to construct new intermediate or even more restrictive logics. In this work, multi-proponent dialogical systems are introduced and adequateness proofs for rules that implement intuitionistic propositional logic and the modal systems S4 and CS4, are provided. Similarities and differences to various sequent systems and dialogical approaches are investigated.