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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13884/
From, Asta Halkjær
Synthetic Completeness for a Terminating Seligman-Style Tableau System
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}
}
