Abstract
We outline benefits of formalizing a proof system for hybrid logic in the proof assistant Isabelle/HOL, showcase how the process of formalization can shape our proofs, and describe our current work on formalizing completeness of a more restrictive system. Formalization: https://devel.isa-afp.org/entries/Hybrid_Logic.html
| Original language | English |
|---|---|
| Publication date | 2020 |
| Publication status | Published - 2020 |
| Event | Advances in Modal Logic 2020 - Virtual event Duration: 24 Aug 2020 → 28 Aug 2020 https://www.helsinki.fi/en/conferences/advances-in-modal-logic-2020 |
Conference
| Conference | Advances in Modal Logic 2020 |
|---|---|
| Location | Virtual event |
| Period | 24/08/2020 → 28/08/2020 |
| Internet address |
Keywords
- Hybrid logic
- Seligman-style tableau
- Isabelle/HOL