猜想、测试与证明：理论探索概述

数学推理的一个关键组成部分是能够针对当前问题领域提出有趣的猜想。在本文中，我们简要概述了一个名为 QuickSpec 的理论探索系统，该系统能够自动发现关于给定函数集的有趣猜想。QuickSpec 通过将项生成与随机测试交替进行来形成候选猜想。通过从较小规模开始并确保仅考虑相对于已发现猜想不可约的项，使得这一过程变得可行。QuickSpec 已成功应用于为自动归纳定理证明生成引理，以及生成函数式程序的规约。我们概述了 QuickSpec 的典型用例，并演示了如何轻松地将其连接到用户选择的定理证明器。