Software Tool Support for Modular Reasoning in Modal Logics of Actions
Samuel Balco (University of Leicester)
Sabine Frittella (Laboratoire d’Informatique Fondamentale d’Orléans)
Giuseppe Greco (Utrecht Institute of Linguistics)
Alexander Kurz (University of Leicester)
A. Palmigiano (TU Delft - Ethics & Philosophy of Technology, University of Johannesburg)
More Info
expand_more
Abstract
We present a software tool for reasoning in and about propositional sequent calculi for modal logics of actions. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. The tool generates embeddings of the calculus in the theorem prover Isabelle/HOL for formalising proofs about D.EAK. Integrating propositional reasoning in D.EAK with inductive reasoning in Isabelle/HOL, we verify the solution of the muddy children puzzle for any number of muddy children. There also is a set of meta-tools that allows us to adapt the software for a wide variety of user defined calculi.
No files available
Metadata only record. There are no files for this record.