Software tool support for modular reasoning in modal logics of actions

## Authors: Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra Palmigiano

## Paper Information

Title: | Software tool support for modular reasoning in modal logics of actions |

Authors: | Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz and Alessandra Palmigiano |

Proceedings: | ITP Papers |

Editors: | Jeremy Avigad and Assia Mahboubi |

Keywords: | dynamic epistemic logic, proof theory of modal logic, interactive theorem proving, Isabelle |

Abstract: | 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 for formalising proofs about D.EAK. Integrating propositional reasoning in D.EAK with inductive reasoning in Isabelle, we verify in Isabelle 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. |

Pages: | 19 |

Talk: | Jul 09 14:30 (Session 49C) |

Paper: |