Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems.
Simon Colton, Geoff Sutcliffe · 2002
Automated Theorem Proving (ATP) researchers who always use the same problems for testing their systems, run the risk of producing systems that can solve only those problems, and are weak on new problems or applications. Furthermore, as the state-of-the-art in ATP progresses, existing test problems become too easy, and testing on them provides little useful information. It is thus important to regularly nd new and harder problems for testing ATP systems. HR is a program that performs automated theory formation in mathematical domains, such as group theory, quasigroup theory, and ring theory. Given the axioms of the domain...