A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the user's choice.

翻译：数学推理的一个关键组成部分是能够对手头的问题域进行有趣的推测。 在本文中, 我们简要概述了一个称为 QuickSpec 的理论探索系统, 这个系统能够自动发现对某组功能的有趣的推测。 QuickSpec 工作通过通过随机测试来互换术语生成来形成候选的猜想。 通过从小尺寸开始,确保只考虑对已经发现的猜想不可减损的术语, 从而可以进行牵引。 QuickSpec 成功地应用了生成 Lemmas, 用于自动导导导引定词验证和生成功能程序规范。 我们概述了QuickSpec 的典型使用案例, 并演示如何轻易将其与用户选择的理论验证联系起来 。