论文标题
通过理想会员资格的操作员陈述的普遍真理
Universal truth of operator statements via ideal membership
论文作者
论文摘要
我们介绍了一个框架，用于通过验证自由代数中的理想成员资格来证明有关线性操作员的陈述。更具体地说，可以治疗有关前态半具态度中形态身份的任意一阶陈述。我们基于非交通性多项式的计算，提出了此类公式有效性的半决赛程序。这些代数计算会自动合并线性，并从有效的理想会员程序中受益。在框架中，使用多组的一阶逻辑对操作员的域和代码组进行建模。为了从逻辑公式中消除量词和函数符号，我们应用了Herbrand的定理和Ackermann的减少。所产生的公式的有效性被证明与有限的非共同多项式成员有限的理想成员相同。我们解释所有相关概念并讨论计算方面。此外，我们通过证明由计算机代数软件辅助的具体运算符语句来说明我们的框架。
We introduce a framework for proving statements about linear operators by verification of ideal membership in a free algebra. More specifically, arbitrary first-order statements about identities of morphisms in preadditive semicategories can be treated. We present a semi-decision procedure for validity of such formulas based on computations with noncommutative polynomials. These algebraic computations automatically incorporate linearity and benefit from efficient ideal membership procedures. In the framework, domains and codomains of operators are modelled using many-sorted first-order logic. To eliminate quantifiers and function symbols from logical formulas, we apply Herbrand's theorem and Ackermann's reduction. The validity of the resulting formulas is shown to be equivalent to finitely many ideal memberships of noncommutative polynomials. We explain all relevant concepts and discuss computational aspects. Furthermore, we illustrate our framework by proving concrete operator statements assisted by our computer algebra software.
