Lemmas: Generation, Selection, Application

TL;DR

This paper investigates the role of lemmas in automated theorem proving, introducing a system that learns and generates useful lemmas, leading to improved performance and solving a long-standing hard problem.

Contribution

It presents a novel system combining learning technology to generate lemmas, significantly enhancing theorem proving capabilities and solving a problem unsolved for twenty years.

Findings

Improved performance in several theorem proving systems

Successful solving of a long-standing hard problem

Demonstrated effectiveness of lemma generation in proof search

Abstract

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.