Foundations of logic programming in hybrid-dynamic quantum logic

TL;DR

This paper introduces a hybrid-dynamic quantum logic framework capable of naturally representing quantum measurements and evolutions, establishing a foundation for logic programming in quantum computing with promising computational properties.

Contribution

It develops a new hybrid-dynamic logic for quantum programs, proves an initial semantics theorem, and lays the groundwork for executable quantum logic programming languages.

Findings

Significant fragment of the logic has good computational properties.

Initial semantics theorem for satisfiable sets of clauses.

Foundation for logic programming in quantum computing.

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.