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.
Abstract In this paper, we provide a logic to reason about the compatibility structure and contextuality of quantum measurements, using inputs from the Foulis-Randall approach to operational quantum logic and the framework of team semantics. A central feature of quantum systems is that not all physical properties can be observed simultaneously. Thus, we formalize the notion of ‘co-measurability’, which captures exactly when two experimental propositions can be confirmed or refuted by a single measurement setup. We introduce the ‘Logic of Co-measurable Experimental Propositions’ (
LC L C ), which models experimental programs as teams of measurement outcomes. Within this framework, we construct a fragment
LC∗ L C ∗ where the conjunction of two propositions is defined to hold only if they are co-measurable. We show that this restriction naturally recovers the algebraic structure of standard quantum logic. It entails the failure of the distributive laws, which is a key feature of quantum logic. The resulting framework unifies classical and quantum scenarios, offering a logical tool for analyzing contextuality in generalized experimental settings.