Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead

Research output: Contribution to conferencePaperResearchpeer-review

12 Downloads (Pure)


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 languageEnglish
Publication date2020
Publication statusPublished - 2020
EventAdvances in Modal Logic 2020 - Virtual event
Duration: 24 Aug 202028 Aug 2020


ConferenceAdvances in Modal Logic 2020
LocationVirtual event
Internet address


  • Hybrid logic
  • Seligman-style tableau
  • Isabelle/HOL

Cite this