  We explore a simple approach to quantum logic based on hybrid and dynamic
modal logic, where the set of states is given by some Hilbert space. In this
setting, a notion of quantum clause is proposed in a similar way the notion of
Horn clause is advanced in first-order logic, that is, to give logical
properties for use in logic programming and formal specification. We propose
proof rules for reasoning about quantum clauses and we investigate soundness
and compactness properties that correspond to this proof calculus. Then we
prove a Birkhoff completeness result for the fragment of hybrid-dynamic quantum
logic determined by quantum clauses.
