In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.

翻译：在量子信息与计算研究中，符号化方法已被广泛用于对量子态与操作进行人工规范与推理。同时，这些方法对于确保量子算法与程序的自动化推理及验证工具的可扩展性与效率至关重要。然而，目前仍缺乏关于量子数据与操作的符号化规范与推理的形式化理论，这极大地限制了自动化验证技术在量子计算中的实际应用。本文提出了一种称为符号算子逻辑$\mathbf{SOL}$的通用逻辑框架，该框架支持对量子数据与操作进行符号化规范与推理。在此框架中，经典一阶逻辑语言被嵌入到用于规范量子数据与操作（包括其递归定义）的形式算子语言中。这种嵌入允许在选定底层经典数据理论（例如布尔代数或群论）的模意义下推理其性质，从而利用为经典计算开发的现有自动化验证工具。需要强调的是，正是这种将经典一阶逻辑嵌入$\mathbf{SOL}$的机制使得符号化方法成为可能。我们设想该框架能为量子计算与信息在Lean、Coq及相关系统等证明辅助器中的形式化验证与自动定理证明提供概念基础。