Software Tool Support for Modular Reasoning in Modal Logics of Actions
| Autor: | Greco, G., Balco, Samuel, Frittella, Sabine, Kurz, Alexander, Palmigiano, Alessandra, Avigad, J., Mahboubi, A., LS Linguistiek de taalinformatica, ILS LLI |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Computer science
interactive theorem prover proof theory for modal logic HOL 0102 computer and information sciences Mathematical proof computer.software_genre 01 natural sciences Software Sequent 0101 mathematics business.industry Programming language 010102 general mathematics Proof assistant Sequent calculus Inductive reasoning 16. Peace & justice Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Isabelle business computer Dynamic epistemic logic |
| Zdroj: | Interactive Theorem Proving ISBN: 9783319948201 ITP Interactive Theorem Proving, 10895(LNCS), 48. Springer Cham |
| DOI: | 10.1007/978-3-319-94821-8_4 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|