Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)

Asta Halkjær From*, Patrick Blackburn, Jørgen Villadsen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.

Original languageEnglish
Title of host publicationProceedings of 10th International Joint Conference Automated Reasoning
EditorsNicolas Peltier, Viorica Sofronie-Stokkermans
Publication date1 Jan 2020
ISBN (Print)9783030510732
Publication statusPublished - 1 Jan 2020
Event10th International Joint Conference on Automated Reasoning - Virtual, Online
Duration: 29 Jun 20205 Jul 2020
Conference number: 10


Conference10th International Joint Conference on Automated Reasoning
CityVirtual, Online
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12166 LNAI


  • Completeness
  • Hybrid logic
  • Isabelle/HOL
  • Soundness


Dive into the research topics of 'Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)'. Together they form a unique fingerprint.

Cite this