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

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

*Corresponding author

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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.
OriginalsprogEngelsk
TitelAutomated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
RedaktørerNicolas Peltier, Viorica Sofronie-Stokkermans
ForlagSpringer
Publikationsdato2020
Sider474-481
DOI
StatusUdgivet - 2020
BegivenhedInternational Joint Conference on Automated Reasoning 2020 - Le Centre de Colloques, Paris, Frankrig
Varighed: 29 jun. 20206 jul. 2020
https://ijcar2020.org/

Konference

KonferenceInternational Joint Conference on Automated Reasoning 2020
LokationLe Centre de Colloques
LandFrankrig
ByParis
Periode29/06/202006/07/2020
Internetadresse

Emneord

  • Hybrid logic
  • Tableaus
  • Isabelle/HOL
  • Proff assistant
  • Seligman-style
  • Completness
  • Soundness

Citer dette