License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.5
URN: urn:nbn:de:0030-drops-138847
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13884/
Go to the corresponding LIPIcs Volume Portal


From, Asta Halkjær

Synthetic Completeness for a Terminating Seligman-Style Tableau System

pdf-format:
LIPIcs-TYPES-2020-5.pdf (0.8 MB)


Abstract

Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.

BibTeX - Entry

@InProceedings{from:LIPIcs.TYPES.2020.5,
  author =	{From, Asta Halkj{\ae}r},
  title =	{{Synthetic Completeness for a Terminating Seligman-Style Tableau System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13884},
  URN =		{urn:nbn:de:0030-drops-138847},
  doi =		{10.4230/LIPIcs.TYPES.2020.5},
  annote =	{Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL}
}

Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL
Collection: 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Issue Date: 2021
Date of publication: 07.06.2021
Supplementary Material: Model (Isabelle/HOL formalization in the Archive of Formal Proofs (4900+ lines)): https://isa-afp.org/entries/Hybrid_Logic.html archived at: https://archive.softwareheritage.org/swh:1:cnt:5a830ce17c70be797b343d9078bf19c43b0f2145


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI