Conference paper
Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead
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
Language: | English |
---|---|
Year: | 2020 |
Proceedings: | Advances in Modal Logic 2020 |
Types: | Conference paper |
ORCIDs: | From, Asta Halkjær |