An introduction to hybrid-dynamic first-order logic

Speaker: Ionuţ Ţuţu (Royal Holloway, University of London)

Abstract: We propose a hybrid-dynamic first-order logic as a formal
foundation for specifying and reasoning about reconfigurable
systems. As the name suggests, the formalism we develop extends
(many-sorted) first-order logic with features that are common to
hybrid and to dynamic logics. This provides certain key advantages for
dealing with reconfiguration, such as: (a) a signature of nominals,
including operation and relation symbols, that allows references to
specific possible worlds / system configurations – as in the case of
hybrid logics; (b) distinguished signatures of rigid and flexible
symbols, where the rigid symbols are interpreted uniformly across
possible worlds – this supports a rigid form of quantification, which
ensures that variables have the same interpretation regardless of the
possible world where they are evaluated; (c) hybrid terms, which
increase the expressive power of the logic in the context of rigid
symbols; and (d) modal operators over dynamic-logic actions, which are
defined as regular expressions over binary nominal relations. In this
context, we advance a notion of hybrid-dynamic Horn clause and develop
a series of results that lead to an initial-semantics theorem for the
Horn-clause fragment of hybrid-dynamic first-order logic.