Foundations of logic programming in hybrid-dynamic quantum logic
<|reference_start|>Foundations of logic programming in hybrid-dynamic quantum logic: 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.<|reference_end|>
@article{gaina2024foundations,
    title={Foundations of logic programming in hybrid-dynamic quantum logic},
    author={Daniel Gaina},
    journal={arXiv preprint arXiv:2406.02085},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.02085},
    primaryClass={cs.LO}
}