
Formalizing
a
SeligmanStyle
Tableau
System
for
Hybrid
Logic
Title: 
Formalizing a SeligmanStyle Tableau System for Hybrid Logic 
Author:

Asta Halkjær From

Submission date: 
20191220 
Abstract: 
This work is a formalization of soundness and completeness proofs
for a Seligmanstyle tableau system for hybrid logic. The completeness
result is obtained via a synthetic approach using maximally
consistent sets of tableau blocks. The formalization differs from
the cited work in a few ways. First, to avoid the need to backtrack in
the construction of a tableau, the formalized system has no unnamed
initial segment, and therefore no Name rule. Second, I show that the
full Bridge rule is admissible in the system. Third, I start from rules
restricted to only extend the branch with new formulas, including only
witnessing diamonds that are not already witnessed, and show that
the unrestricted rules are admissible. Similarly, I start from simpler
versions of the @rules and show the general ones admissible. Finally,
the GoTo rule is restricted using a notion of coins such that each
application consumes a coin and coins are earned through applications of
the remaining rules. I show that if a branch can be closed then it can
be closed starting from a single coin. These restrictions are imposed
to rule out some means of nontermination. 
BibTeX: 
@article{Hybrid_LogicAFP,
author = {Asta Halkjær From},
title = {Formalizing a SeligmanStyle Tableau System for Hybrid Logic},
journal = {Archive of Formal Proofs},
month = dec,
year = 2019,
note = {\url{http://isaafp.org/entries/Hybrid_Logic.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

