 As mentioned above, the papers Blackburn, Bolander, Braüner, and Jørgensen (2017) and Jørgensen, Blackburn, Bolander, Braüner (2016) gave completenes proofs for Seligman-style tableau systems for hybrid logic. Based on these results, completeness for these systems have in From (2021) and From, Blackburn, and Villadsen (2020) been fully formalised using the proof assistant Isabelle/HOL.