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.

翻译：我们探索一种基于混合与动态模态逻辑的量子逻辑简单方法，其中状态集由某个希尔伯特空间给出。在此框架下，我们以类似于一阶逻辑中提出 Horn 子句概念的方式，引入了量子子句的概念，旨在为逻辑编程与形式化规范提供逻辑属性。我们提出了用于推理量子子句的证明规则，并研究了与此证明演算相对应的可靠性与紧致性。随后，我们证明了由量子子句确定的混合动态量子逻辑片段具有 Birkhoff 完备性。