Software Tool Support for Modular Reasoning in Modal Logics of Actions

None, None; None, None; None, None; None, None; None, None

Software Tool Support for Modular Reasoning in Modal Logics of Actions

Conference Paper (2018)

Author(s)

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)

Alessandra Palmigiano (TU Delft - Technology, Policy and Management, University of Johannesburg)

Research Group

Ethics & Philosophy of Technology

DOI related publication

https://doi.org/10.1007/978-3-319-94821-8_4 Final published version

To reference this document use

https://resolver.tudelft.nl/uuid:03d3ee57-3728-4d07-840e-b15ef543c58b

More Info

expand_more

Publication Year

2018

Language

English

Research Group

Ethics & Philosophy of Technology

Volume number

10895 LNCS

Pages (from-to)

48-67

Publisher

Springer

ISBN (print)

9783319948201

Event

9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 (2018-07-09 - 2018-07-12), Oxford, United Kingdom

Downloads counter

155

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.