Proof search in multi-agent dialogues for modal logic

Auteurs

• Martin Sticht

Paramètres

• Informatique, programmation

En savoir plus sur le livre

In computer science, modal logics are crucial for modeling knowledge structures and ontologies, with intuitionistic or constructive propositional logic being a specific type. Constructive modal logics represent a restrictive family of modal systems, and various reasoning procedures have been explored to prove the validity of statements within these logics. Aiming for normalized deductions, a novel approach leads to dialogical logic, a game-theoretic reasoning technique involving two players: a proponent and an opponent. The proponent presents an assertion as a formula, and the game rules can be adjusted for flexibility. Introducing additional proponent-players to challenge one opponent in a round-based format facilitates proof normalization. Ordinary sequent systems can be adapted to this dialectic framework to achieve such normalization. Moreover, the round-based structure allows for parallelization of the reasoning process. By modifying game rules, new intermediate or more restrictive logics can be developed. This work introduces multi-proponent dialogical systems and provides adequateness proofs for rules implementing intuitionistic propositional logic and the modal systems S4 and CS4, while examining the similarities and differences with various sequent systems and dialogical approaches.

Achat du livre

• Année de publication: 2018