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

Abstract

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
PublisherSpringer
Publication date1 Jan 2020
Pages474-481
ISBN (Print)9783030510732
DOIs
Publication statusPublished - 1 Jan 2020
Event10th International Joint Conference on Automated Reasoning - Virtual, Online
Duration: 29 Jun 20205 Jul 2020
Conference number: 10

Conference

Conference10th International Joint Conference on Automated Reasoning
Number10
CityVirtual, Online
Period29/06/202005/07/2020
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12166 LNAI
ISSN0302-9743

Keywords

  • Completeness
  • Hybrid logic
  • Isabelle/HOL
  • Soundness

Cite this