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

Ethics & Philosophy of Technology

Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

2 Citations (Scopus)

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
Publisher	Springer
Pages	48-67
Number of pages	20
Volume	10895 LNCS
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_4
Publication status	Published - 2018
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

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 Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (Vol. 10895 LNCS, pp. 48-67). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS). Springer. 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. Vol. 10895 LNCS Springer, 2018. pp. 48-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{03d3ee5737284d07840eb15ef543c58b,

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

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

language = "English",

isbn = "9783319948201",

volume = "10895 LNCS",

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

publisher = "Springer",

pages = "48--67",

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

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 Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. vol. 10895 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10895 LNCS, Springer, 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. Vol. 10895 LNCS Springer, 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/Conference proceedings/Edited volume › Conference contribution › Scientific › 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

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.

UR - http://www.scopus.com/inward/record.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

VL - 10895 LNCS

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

PB - Springer

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 Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Vol. 10895 LNCS. Springer. 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

Other files and links

Fingerprint

Cite this