Axiomatization of Hybrid Logic of Link Variations

In this paper, we investigate local and global dynamic modal operators which have the ability to update the accessibility relation of a model. For the global operators, the logic \(\textsf{GLV}\) of global link variations based on hybrid logic \(\textsf{H}(@)\) is introduced, which involves global link cutting, adding and rotating simultaneously. A Hilbert-style calculus \(\mathsf {C_{GLV}}\) is provided. By constructing families of canonical models inductively, we prove that the calculus \(\mathsf {C_{GLV}}\) is sound and strongly complete with respect to \(\textsf{GLV}\) . For the local operators, we extended the logic \(\textsf{LLD}(@,\downarrow \ )\) of link deletion introduced in [12] to \(\textsf{LLV}\) , which is based on the hybrid logic \(\textsf{H}(\textsf{E},\downarrow \ )\) and involves local definable link cutting, adding and rotating. By defining local named dynamic operators and providing recursion axioms for them, we obtain a sound and strongly complete calculus \(\mathsf {C_{LLV}}\) for \(\textsf{LLV}\) . Moreover, we show that for an arbitrary set X of global and local dynamic operators, the calculus \(\mathsf {C_{GLV}}(X)\) and \(\mathsf {C_{LLV}}(X)\) are still sound and strongly complete w.r.t the logic \(\textsf{GLV}(X)\) and \(\textsf{LLV}(X)\) , respectively.