通过证明可调查性，我理解人类用户可以“追踪”证明的所有细节这一事实。有些事情不容易追踪。例如，SMT 证明基于特定的启发式，然后将其转换为证明者。在这种情况下，拥有简单的机制（无需专家即可让您使用）来扫描证明失败的原因或检查证明过程的内部结构可能很有用。
我想知道与 Coq 或 Isabelle 相比，Lean 是否增强了这种证明可测量性。我通过A Metaprogramming Framework for Formal Verification得到的印象可能是这种情况。
问问题
179 次
1 回答
1
如果我正确理解proof-surveyability 或-traceability，那么根据定义，完全详细的证明是“100% 可追溯的”，而仅仅说明结果（例如引理）是“0% 可追溯”。
在那种情况下，我不明白为什么 Lean 会比 Coq 或 Isabelle 或任何其他核心目的是检查完整详细证明的正确性的工具有所改进。此类工具通常提供提高自动化的方法，这很方便，但可以说会降低可追溯性，具体取决于如何表示额外的证明步骤。例如，类似 Coq 的策略可以提高自动化程度，但可以“恢复”可追溯性，因为策略推断的步骤可以以与显式提供的步骤相同的方式表示：作为证明规则应用程序或演绎步骤。
后一部分对于 SMT 推断的证明步骤是困难的：与 Coq 等证明检查器相比，SMT 求解器可以实现更高程度的自动化，但是以可追溯性为代价，因为它的“推理”更多是技术性的，更少的人为- 类似/演绎。
顺便说一句：证明检查器和 SMT 求解器之间的这种差异让我想起了经典图像识别和基于 AI 的图像识别之间的差异。前者自动化/效率较低，但更容易追踪/解释。
于 2020-09-01T12:39:33.523 回答