Software Tool Support for Modular Reasoning in Modal Logics of Actions

G. Greco; Samuel Balco; Sabine Frittella; Alexander Kurz; Alessandra Palmigiano

doi:10.1007/978-3-319-94821-8_4

Software Tool Support for Modular Reasoning in Modal Logics of Actions

G. Greco, Samuel Balco, Sabine Frittella, Alexander Kurz, Alessandra Palmigiano

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Interactive Theorem Proving
Subtitle of host publication	9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
Editors	J. Avigad, A. Mahboubi
Publisher	Springer
Pages	48-67
Volume	10895
Edition	LNCS
ISBN (Electronic)	978-3-319-94821-8
ISBN (Print)	978-3-319-94820-1
DOIs	https://doi.org/10.1007/978-3-319-94821-8_4
Publication status	Published - 2018

Keywords

Dynamic epistemic logic
interactive theorem prover
Isabelle
proof theory for modal logic

Access to Document

10.1007/978-3-319-94821-8_4

Balco2018_Chapter_SoftwareToolSupportForModularRFinal published version, 575 KB

Cite this

Greco, G., Balco, S., Frittella, S., Kurz, A., & Palmigiano, A. (2018). Software Tool Support for Modular Reasoning in Modal Logics of Actions. In J. Avigad, & A. Mahboubi (Eds.), Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (LNCS ed., Vol. 10895, pp. 48-67). Springer. https://doi.org/10.1007/978-3-319-94821-8_4

Greco, G. ; Balco, Samuel ; Frittella, Sabine et al. / Software Tool Support for Modular Reasoning in Modal Logics of Actions. Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. editor / J. Avigad ; A. Mahboubi. Vol. 10895 LNCS. ed. Springer, 2018. pp. 48-67

@inproceedings{6ae47495a802400388c2e156a29ab02b,

title = "Software Tool Support for Modular Reasoning in Modal Logics of Actions",

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.",

keywords = "Dynamic epistemic logic, interactive theorem prover, Isabelle, proof theory for modal logic",

author = "G. Greco and Samuel Balco and Sabine Frittella and Alexander Kurz and Alessandra Palmigiano",

year = "2018",

doi = "10.1007/978-3-319-94821-8_4",

language = "English",

isbn = "978-3-319-94820-1",

volume = "10895",

pages = "48--67",

editor = "J. Avigad and A. Mahboubi",

booktitle = "Interactive Theorem Proving",

publisher = "Springer",

address = "Germany",

edition = "LNCS",

}

Greco, G, Balco, S, Frittella, S, Kurz, A & Palmigiano, A 2018, Software Tool Support for Modular Reasoning in Modal Logics of Actions. in J Avigad & A Mahboubi (eds), Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. LNCS edn, vol. 10895, Springer, pp. 48-67. https://doi.org/10.1007/978-3-319-94821-8_4

Software Tool Support for Modular Reasoning in Modal Logics of Actions. / Greco, G.; Balco, Samuel; Frittella, Sabine et al.
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. ed. / J. Avigad; A. Mahboubi. Vol. 10895 LNCS. ed. Springer, 2018. p. 48-67.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Software Tool Support for Modular Reasoning in Modal Logics of Actions

AU - Greco, G.

AU - Balco, Samuel

AU - Frittella, Sabine

AU - Kurz, Alexander

AU - Palmigiano, Alessandra

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Dynamic epistemic logic

KW - interactive theorem prover

KW - Isabelle

KW - proof theory for modal logic

U2 - 10.1007/978-3-319-94821-8_4

DO - 10.1007/978-3-319-94821-8_4

M3 - Conference contribution

SN - 978-3-319-94820-1

VL - 10895

SP - 48

EP - 67

BT - Interactive Theorem Proving

A2 - Avigad, J.

A2 - Mahboubi, A.

PB - Springer

ER -

Greco G, Balco S, Frittella S, Kurz A, Palmigiano A. Software Tool Support for Modular Reasoning in Modal Logics of Actions. In Avigad J, Mahboubi A, editors, Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. LNCS ed. Vol. 10895. Springer. 2018. p. 48-67 doi: 10.1007/978-3-319-94821-8_4

Software Tool Support for Modular Reasoning in Modal Logics of Actions

Abstract

Keywords

Access to Document

Fingerprint

Cite this