自动推理系统和辅助证明系统的区别

林一二2023年07月01日 12:11

定理机器证明的重点是“发现”方面。追求功率和效率,往往以牺牲稳定性为代价。这样的系统可能有错误,并且很难确保它们交付的结果是正确的。相比之下,交互式定理证明主要集中在定理证明的“验证”方面,要求在适当的公理基础上证明每一个主张。

Code
定理机器证明的重点是“发现”方面。追求功率和效率,往往以牺牲稳定性为代价。这样的系统可能有错误,并且很难确保它们交付的结果是正确的。相比之下,交互式定理证明主要集中在定理证明的“验证”方面,要求在适当的公理基础上证明每一个主张。