HR to TPTP
Abstract
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 find 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, HR invents concepts, finds examples of them using a model
generator, and makes conjectures empirically about the concepts. HR
has been used to discover new group theory theorems of sufficient
difficulty to be included in the TPTP - the standard library of test
problems for first order ATP systems. As HR produces tens of
thousands of distinct theorems, there has also been an opportunity to
determine some characteristics that can be used to identify hard problems.