|
Formalizing
a
Seligman-Style
Tableau
System
for
Hybrid
Logic
Title: |
Formalizing a Seligman-Style Tableau System for Hybrid Logic |
Author:
|
Asta Halkjær From
|
Submission date: |
2019-12-20 |
Abstract: |
This work is a formalization of soundness and completeness proofs for
a Seligman-style 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 derivable 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 derivable. Similarly, I start from simpler
versions of the @-rules and derive the general ones. These
restrictions are imposed to rule out some means of nontermination. |
BibTeX: |
@article{Hybrid_Logic-AFP,
author = {Asta Halkjær From},
title = {Formalizing a Seligman-Style Tableau System for Hybrid Logic},
journal = {Archive of Formal Proofs},
month = dec,
year = 2019,
note = {\url{http://isa-afp.org/entries/Hybrid_Logic.html},
Formal proof development},
ISSN = {2150-914x},
}
|
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.
|
|