2026/01/01 by Christoph Wernhard
#cs.LO
paper · pdf · doi:10.1007/978-3-032-32589-1_3
Abstract We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment. This ties in with automated first-order proving by proof structure enumeration, and links to Metamath and formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets, and incorporating combinators into proof terms. Our lemmas significantly improve solution rates of provers, e.g., of Vampire from 74% to 94%, and of leanCoP from 7% to 44%.