Software Tool Support for Modular Reasoning in Modal Logics of Actions

Samuel Balco; Sabine Frittella; Giuseppe Greco; Alexander Kurz; Alessandra Palmigiano

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

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 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 - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Jeremy Avigad, Assia Mahboubi
Publisher	Springer Verlag
Pages	48-67
Number of pages	20
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_4
Publication status	Published - 1 Jan 2018
Externally published	Yes
Event	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Publication series

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

Conference

Conference	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

Access to Document

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

Handle.net

Persistent link

Cite this

Balco, S., Frittella, S., Greco, G., 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, Proceedings (pp. 48-67). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_4

Balco, Samuel ; Frittella, Sabine ; Greco, Giuseppe 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, Proceedings. editor / Jeremy Avigad ; Assia Mahboubi. Springer Verlag, 2018. pp. 48-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2631f2a5b51e43e48544cb2af4b2f4fa,

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

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

year = "2018",

month = jan,

day = "1",

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

language = "English",

isbn = "9783319948201",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "48--67",

editor = "Jeremy Avigad and Assia Mahboubi",

booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

address = "Germany",

note = "9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

}

Balco, S, Frittella, S, Greco, G, 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, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10895 LNCS, Springer Verlag, pp. 48-67, 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1007/978-3-319-94821-8_4

Software Tool Support for Modular Reasoning in Modal Logics of Actions. / Balco, Samuel; Frittella, Sabine; Greco, Giuseppe et al.

Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Jeremy Avigad; Assia Mahboubi. Springer Verlag, 2018. p. 48-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS).

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 - Balco, Samuel

AU - Frittella, Sabine

AU - Greco, Giuseppe

AU - Kurz, Alexander

AU - Palmigiano, Alessandra

PY - 2018/1/1

Y1 - 2018/1/1

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.

UR - http://www.scopus.com/inward/record.url?scp=85049921153&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85049921153&partnerID=8YFLogxK

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

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

M3 - Conference contribution

AN - SCOPUS:85049921153

SN - 9783319948201

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 48

EP - 67

BT - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Avigad, Jeremy

A2 - Mahboubi, Assia

PB - Springer Verlag

T2 - 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 9 July 2018 through 12 July 2018

ER -

Balco S, Frittella S, Greco G, 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, Proceedings. Springer Verlag. 2018. p. 48-67. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-94821-8_4

Software Tool Support for Modular Reasoning in Modal Logics of Actions

Abstract

Publication series

Conference

Access to Document

Handle.net

Other files and links

Fingerprint

Cite this