Software Tool Support for Modular Reasoning in Modal Logics of Actions

Conference paper (2018)

Authors

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 , University of Johannesburg
More Info
expand_more

Published Date

2018

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

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.

Files

Balco2018_Chapter_SoftwareTool... (pdf)
(pdf | 0.648 Mb)

Download not available