《约化环定理》中的数学理论探索
Mathematical Theory Exploration in Theorema: Reduction Rings
摘要：
在本文中，我们提出了有史以来第一次计算机形式化的理论，格罗布纳基在约化环，这是一个重要的理论在计算交换代数，定理。不仅形式化，而且所有结果的形式化验证也已全部完成，特别是Buchberger算法在约化环上的一般实现和正确性证明。得益于Theorema中证明和计算的无缝集成，该实现现在可以直接在系统内计算各种不同域中的格罗布纳基。此外，我们的形式化的很大一部分是完全由“基本理论”，如集合，数字和元组，它们本身独立于约化环，因此可以作为未来理论探索的基础。此外，我们还报告了两个通用的Theorema工具，我们开发了一个有效的和方便的探索数学理论：一个互动的证明策略和“理论分析器”，已经证明非常有用的时候，创建大型结构化的知识库。
英文摘要：
In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchberger's algorithm in reduction rings. Thanks to the seamless integration of proving and computing in Theorema, this implementation can now be used to compute Gröbner bases in various different domains directly within the system. Moreover, a substantial part of our formalization is made up solely by "elementary theories" such as sets, numbers and tuples that are themselves independent of reduction rings and may therefore be used as the foundations of future theory explorations in Theorema. In addition, we also report on two general-purpose Theorema tools we developed for an efficient and convenient exploration of mathematical theories: an interactive proving strategy and a "theory analyzer" that already proved extremely useful when creating large structured knowledge bases.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
