Foundations of logic programming in hybrid-dynamic quantum logic
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.
Cite
@article{arxiv.2406.02085,
title = {Foundations of logic programming in hybrid-dynamic quantum logic},
author = {Daniel Gaina},
journal= {arXiv preprint arXiv:2406.02085},
year = {2024}
}