ACL2中的代数基本定理

下载 PDF 摘要：我们报告了对 ACL2(r) 中代数基本定理的验证。该证明由四部分组成。首先，定义了复数的复值函数和实值函数的连续性，表明从复数到实数的连续函数在封闭的正方形区域内达到最小值。连续实值复函数的一个重要例子是取连续复函数的传统复范数。我们认为这些连续函数只有一个（复数）参数，但在 ACL2(r) 中它们表现为两个参数的函数。额外的参数是未解释的“上下文”。例如，它可以是固定的其他参数，如具有底数和指数的指数函数，其中任何一个都可以固定。第二，证明复多项式是连续的，因此复多项式的范数是一个连续的实值函数，它在以原点为中心的任意正方形区域上达到其最小值。这部分证明受益于“上下文”参数的引入，它说明了一个创新，它简化了具有未绑定参数的经典属性的证明。第三，我们推导出离原点足够远的输入的非常量多项式范数的下限和上限。这意味着可以找到一个足够大的平方来保证它包含多项式范数的全局最小值。第四，表明如果给定的数不是非常量多项式的根，则它不可能是全局最小值。最后，将这些结果结合起来，表明全局最小值必须是多项式的根。这个结果是 ACL2(r) 中复杂多项式形式化的更大努力的一部分。