如何自动化算子命题的证明：以穆尔-彭罗斯逆为例
符号计算
2023-06-28 v2 计算机科学中的逻辑
摘要
我们描述了一种近期发展的代数框架，用于通过对非交换多项式的计算来证明关于线性算子的初等命题。此外，我们展示了新的 SageMath 包 operator_gb，它提供了自动化此类计算的功能。我们旨在通过示例提供对我们方法及软件的实用性理解，同时解释该方法的完备性——即它允许为每一个为真的初等算子命题找到代数证明。我们通过关于穆尔-彭罗斯逆命题的案例分析（包含经典事实与近期结果，以在线笔记本形式呈现）来说明该框架结合我们软件的能力。
引用
@article{arxiv.2305.09448,
title = {How to automatise proofs of operator statements: Moore-Penrose inverse -- a case study},
author = {Klara Bernauer and Clemens Hofstadler and Georg Regensburger},
journal= {arXiv preprint arXiv:2305.09448},
year = {2023}
}
备注
22 pages, plus 8 additional pages appendix