Birkhoff style calculi for hybrid logics

Abstract

Abstract We develop an abstract proof calculus for hybrid logics whose sentences are ( hybrid ) Horn clauses , and we prove a Birkhoff completeness theorem for hybrid logics in the general setting provided by the institution theory . This result is then applied to particular cases of hybrid logics with user-defined sharing, where the first-order variables in quantified sentences are interpreted uniformly across worlds.