The Homer System

摘要

The Homer system combines the HR automated theory formation program [2], the Otter theorem prover [6], and the Maple computer algebra package [1] to make intelligent conjectures about number theory functions supplied by the user. The integration is as follows: given Maple code for some functions the user is interested in, Maple is used to calculate values for those functions. HR then forms a theory using the functions as background knowledge, calling Maple whenever necessary to perform additional calculations. The theory formation process makes conjectures empirically and the user is initially asked to prove or disprove each conjecture. As the theory formation progresses, however, Homer uses the theorems it has found (namely those proved by the user) as axioms in attempts to prove the conjectures itself using Otter. Any conjectures proved in this way are likely to follow easily from the theorems already known to the user, so Homer does not present them, in order to keep the quality of the output high. Using Otter in this extreme way is not meant to indicate that Otter can only prove trivial theorems, nor that HR produces too many dull conjectures. Rather, we wish to emphasise the power of the combined system (Homer) at discovering interesting conjectures by generate (HR) and quick test (Otter).