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.

翻译：本文的主要贡献是引入了一种简单而富有表达力的混合动态逻辑，用于描述量子程序。该版本的量子逻辑能够基于（混合与动态）模态逻辑中提出的概念，自然地表达量子测量和状态的幺正演化。随后，我们研究了所提出的混合动态量子逻辑中的Horn子句，并发展了一系列结果，最终为可满足的子句集建立了初始语义定理。这表明混合动态量子逻辑的一个重要片段具有良好的计算性质，可以作为定义用于规约量子程序的可执行语言的基础。我们通过证明Herbrand定理的一个变体，为该片段中的逻辑编程奠定了基础，该定理将逻辑编程查询相对于程序的语义蕴涵问题约简为寻找合适代换的搜索问题。