Foundations of logic programming in hybrid-dynamic quantum logic
Daniel Gaina
TL;DR
The paper develops Hybrid-Dynamic Quantum Logic (HDQL) as a modular, expressive foundation for describing and reasoning about quantum programs within a Hilbert-space setting. It integrates unitary evolutions and projective measurements into a two-layer, hybrid-dynamic modal framework with both local and global satisfaction notions, enabling formal verification and specification of quantum protocols. A key contribution is establishing initial semantics for satisfiable Horn-clause sets and proving a variant of Herbrand's theorem that reduces semantic entailment to an existential search for an answer substitution, thus supporting executable, rewrite-based reasoning in quantum contexts. Collectively, these results lay the groundwork for logic programming approaches to quantum software, providing a principled route from semantic models to syntactic, substitution-driven execution.
Abstract
The main contribution of the present paper is the introduction of a simple yet expressive hybrid-dynamic logic for describing quantum programs. This version of quantum logic can express quantum measurements and unitary evolutions of states in a natural way based on concepts advanced in (hybrid and dynamic) modal logics. We then study Horn clauses in the hybrid-dynamic quantum logic proposed, and develop a series of results that lead to an initial semantics theorem for sets of clauses that are satisfiable. This shows that a significant fragment of hybrid-dynamic quantum logic has good computational properties, and can serve as a basis for defining executable languages for specifying quantum programs. We set the foundations of logic programming in this fragment by proving a variant of Herbrand's theorem, which reduces the semantic entailment of a logic-programming query by a program to the search of a suitable substitution.