| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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 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_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{https://isa-afp.org/entries/Hybrid_Logic.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|