Horn Clauses in Hybrid-Dynamic First-Order Logic

TL;DR

This paper introduces a hybrid-dynamic first-order logic framework with Horn clauses, enabling formal reasoning about reconfigurable systems, and demonstrates its computational properties and potential for logic programming applications.

Contribution

It extends first-order logic with hybrid and dynamic features, develops a semantics for Horn clauses, and establishes a foundation for logic programming in reconfigurable systems.

Findings

Initial-semantics theorem for clause sets

Good computational properties of the logic fragment

Foundation for logic programming in reconfigurable systems

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 logics and to dynamic logics. This provides certain key advantages for dealing with reconfigurable systems, 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. We then study Horn clauses in this hybrid-dynamic logic, and develop a series of results that lead to an initial-semantics theorem for arbitrary sets of clauses. This shows that a significant fragment of hybrid-dynamic first-order logic has good computational properties, and can serve as a basis for defining executable languages for reconfigurable systems. Lastly, we set out the foundations of logic programming in this fragment by proving a hybrid-dynamic variant of Herbrand's theorem, which reduces the semantic entailment of a logic-programming query by a program to the search of a suitable answer substitution.