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

Research output: Contribution to conferencePaperResearchpeer-review

12 Downloads (Pure)

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 languageEnglish
Publication date2020
Publication statusPublished - 2020
EventAdvances in Modal Logic 2020 - Virtual event
Duration: 24 Aug 202028 Aug 2020
https://www.helsinki.fi/en/conferences/advances-in-modal-logic-2020

Conference

ConferenceAdvances in Modal Logic 2020
LocationVirtual event
Period24/08/202028/08/2020
Internet address

Keywords

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

Cite this