Email Gateway (Aug 23 2022 at 08:14): Email Gateway (Aug 23 2022 at 08:14):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Formalizing a Seligman-Style Tableau System for Hybrid Logic
by Asta Halkjær From
https://www.isa-afp.org/entries/Hybrid_Logic.html
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.
Enjoy!
Gerwin
Last updated: Apr 24 2024 at 12:33 UTC