如何解决精益提高了证明的可测量性吗?
通过证明可调查性,我了解一个事实,即人类用户可以“追踪”证明的所有细节。有些事情不容易追查。例如,SMT证明基于特定的启发式方法,然后将其转换为证明者。在这种情况下,使用简单的机制(无需专家来处理)可能有用,以扫描证明失败的原因或检查证明程序的内部结构。
我想知道,与Coq或Isabelle相比,Lean是否增强了这种证明可测量性。我的印象是,通过用于形式验证的元编程框架可以浏览这种情况。
解决方法
如果我正确理解证明的可测量性或可追溯性,那么根据定义,完全详细的证明是“ 100%可追溯的”,而仅说明结果(例如引理)是“ 0%可追溯的”。
在那种情况下,我看不出Lean为什么会比Coq或Isabelle或其他任何主要目的是检查完整详细证明的正确性的工具有所改进。这样的工具通常提供增加自动化的手段,这很方便,但是可以说取决于可证明额外证明步骤的方式降低了可追溯性。例如。类似于Coq的策略可以提高自动化程度,但是可以“恢复”可追溯性,因为可以以与明确提供的步骤相同的方式表示策略推断的步骤:作为证明规则应用程序或推论步骤。
对于SMT推导的证明步骤,后一部分比较困难:与Coq等证明检查器相比,SMT求解器可以实现更高的自动化程度,但以可追溯性为代价,因为其“推理”技术性更高而不像人一样/演绎。
作为一个补充说明:证明检查器和SMT求解器之间的这种差异使我想起了经典图像识别和基于AI的图像识别之间的差异。前者自动化程度较低/效率较低,但更易于跟踪/解释。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。