Experiments with the hot list strategy

Experimentation strongly suggests that, for attacking deep questions and hard problems with the assistance of an automated reasoning program, the more effective paradigms rely on the retention of deduced information. A significant obstacle ordinarily presented by such a paradigm is the deduction and retention of one or more needed conclusions whose complexity sharply delays their consideration. To mitigate the severity of the cited obstacle, the author formulates and features in this report the hot list strategy. The hot list strategy asks the researcher to choose, usually from among the input statements, one or more clauses that are conjectured to play a key role for assignment completion. The chosen clauses - conjectured to merit revisiting, again and again - are placed in an input list of clauses, called the hot list. When an automated reasoning program has decided to retain a new conclusion C - before any other clause is chosen to initiate conclusion drawing - the presence of a nonempty hot list (with an appropriate assignment of the input parameter known as heat) causes each inference rule in use to be applied to C together with the appropriate number of members of the hot list. Members of the hot list are used to complete applications of inference rules and not to initiate applications. The use of the hot list strategy thus enables an automated reasoning program to briefly consider a newly retained conclusion whose complexity would otherwise prevent its use for perhaps many CPU-hours. To give evidence of the value of the strategy, the author focuses on four contexts: (1) dramatically reducing the CPU time required to reach a desired goal; (2) finding a proof of a theorem that had previously resisted all but the more inventive automated attempts; (3) discovering a proof that is more elegant than previously known; and (4) answering a question that had steadfastly eluded researchers relying on an automated reasoning program