Software Tool Support for Modular Reasoning in Modal Logics of Actions

Samuel Balco*, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsJeremy Avigad, Assia Mahboubi
PublisherSpringer Verlag
Pages48-67
Number of pages20
ISBN (Print)9783319948201
DOIs
Publication statusPublished - 1 Jan 2018
Externally publishedYes
Event9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10895 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Fingerprint

Dive into the research topics of 'Software Tool Support for Modular Reasoning in Modal Logics of Actions'. Together they form a unique fingerprint.

Cite this