Formalizing a Seligman-Style TableauSystem for Hybrid Logic (Short Paper)

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

*Corresponding author

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

Abstract

Hybrid logic is modal logic enriched with names for worlds.We formalize soundness and completeness proofs for a Seligman-styletableau system for hybrid logic in the proof assistant Isabelle/HOL. Theformalization shows how to lift certain rule restrictions, thereby simpli-fying the original un-formalized proof. Moreover, the completeness proofwe formalize is synthetic which suggests we can extend this work to provea wider range of results about hybrid logic.
Original languageEnglish
Title of host publicationAutomated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
EditorsNicolas Peltier, Viorica Sofronie-Stokkermans
PublisherSpringer
Publication date2020
Pages474-481
DOIs
Publication statusPublished - 2020
EventInternational Joint Conference on Automated Reasoning 2020 - Le Centre de Colloques, Paris, France
Duration: 29 Jun 20206 Jul 2020
https://ijcar2020.org/

Conference

ConferenceInternational Joint Conference on Automated Reasoning 2020
LocationLe Centre de Colloques
CountryFrance
CityParis
Period29/06/202006/07/2020
Internet address

Keywords

  • Hybrid logic
  • Tableaus
  • Isabell/HOL
  • Proof assistant
  • Seligman-style
  • Completness
  • Soundness

Cite this