When a mathematician or logician is seeking a proof of a purported theorem, quite often lemmas play a key role in the research. Two sources exist for such lemmas: (1) they may be included at the beginning (as part of the so-called input), or (2) they may be deduced and adjoined to the pool of information. Whether such lemmas are present at the start or proved during the search for a proof typically has little or no effect on the likelihood of success by the researcher. Such is not the case, however, for automated reasoning programs. Indeed, for all of the reasoning programs known to me, a sharp practical difference exists when comparing lemma inclusion (in the input) with lemma adjunction (during the run) resulting from the program's reasoning. (Lemma adjunction in this discussion in no way refers to what occurs when using the dynamic hot list strategy, in which a retained conclusion is adjoined to the hot list.) In this article, I discuss the nature of that difference, its effect on success in problem solving, and a possible strategy for identifying and utilizing key lemmas.

Key Lemmas and Their Children

Let me begin with a brief review of the nature of lemmas in proof finding. When a lemma turns out to play a key role in producing a sought-after proof, that lemma alone almost never suffices. In particular, in addition to the presence of the lemma in the proof, also present are conclusions that have as an immediate parent the cited lemma. If such conclusions are thought of as children of the lemma, often grandchildren are present and even later descendants. In other words, the lemma is only the first element in a line of reasoning whose other elements are also crucial.

The researcher, either explicitly or implicitly, notes the origin of a conclusion. Thus, the researcher has knowledge of the inherited importance of that conclusion and, if such is the choice, can use that knowledge to direct the search for a proof. The reasoning program does not have such knowledge. To be precise, the program has knowledge of the parental history of conclusions in order to present a proof should one be found; but, although it is aware of the importance of each conclusion through the use of weighting that in turn assigns priorities, it is not aware of inherited importance resulting from the importance of ancestors in the derivation tree of a conclusion. How, then, has a reasoning program such as Otter been so successful?

The Use of Strategies for Identifying Key Lemmas

One explanation for Otter's success rests with the diverse strategies the reasoning program offers. Indeed, Otter has several strategies that provide aid in focusing on key lemmas. One such strategy--the resonance strategy [Wos1995]--works in the following way.

The user of Otter includes (in the input) a resonator (a formula or equation whose variables are treated as indistinguishable) for each of the lemmas conjectured to play a key role if and when proved during the run. When such a key lemma is proved (that matches a resonator), it will be assigned a value (priority) identical to that given the matching resonator. If a small value (high priority) has been assigned to the corresponding input resonator, then the lemma will be given high priority for initiating applications of the chosen inference rules.

Through the use of the resonance strategy, then, Otter seems to offer just what is needed to quickly turn to a proved lemma thought to be key and pursue a line of reasoning whose first element is that lemma. In practice, however, a different situation occurs. When the program deduces and retains such a lemma, as is the case in mathematics or in logic, seldom is it the last step of the sought-after proof. Almost as seldom is the case in which the key lemma is chosen as the focus of attention to draw further conclusions one of which completes the desired proof. Instead, in the vast majority of cases concerned with completing a proof, the so-called key lemma initiates a line of reasoning whose other elements also play a crucial role, occasionally ending with the last step of the proof. The resonance strategy is relevant only to the identification of potentially key lemmas, the first step of such lines of reasoning; it provides no aid with regard to focusing on the progeny of such identified conclusions (unless by accident a descendant also matches some included resonator).

The user familiar with Otter might argue that a combination of the resonance strategy and the ratio strategy provides the desired capability. The ratio strategy [McCune1992] combines a breadth-first search with a search based on the complexity of retained conclusions. It is a powerful means for enabling an automated reasoning program to occasionally focus on long clauses that it would otherwise ignore for much CPU time, or forever. But can it, together with the resonance strategy, offer what is needed? Consider the following two cases in which both the resonance strategy and the ratio strategy are used.

In the first case, success seems assured. Let A, the clause equivalent of a key lemma, be included in the input. Instruct Otter to consider all clauses in the initial set of support (before any deduced clause) to initiate inference-rule applications. Then, as the following illustrates, any new conclusion that is retained and that has A as one of its parents has an excellent chance of being chosen reasonably early to be used to draw further conclusions. Let such a child-clause be called B. When retained, it might be given the clause number, say, 500. Therefore, even if B would ordinarily be delayed for consideration as an initiator because of its complexity, the use of the ratio strategy with a small assigned value (such as 4 or less) will quickly bring it to the attention of the program. In the case under discussion, use of the resonance strategy coupled with the ratio strategy enables the program to compete well with the researcher and to behave rather similarly. Indeed, the researcher is quite likely to focus heavily on B (derived in part from A) because of being so closely related to a conjectured-to-be key lemma. The reasoning program can do the same (through the use of the resonance strategy) if it happened to have an appropriate resonator in its input. On the other hand, the early choosing of A would not influence the program in choosing B, even if A had been chosen because the program had been told (for example, through the use of the resonance strategy) that A might play a key role.

However, consider what happens in the following case. If, rather than being an included lemma, A is instead an adjoined lemma given, say, the clause number 1000, then B may well be assigned the clause number 20,000. In that event, the program will delay for a very long CPU time-perhaps forever-before focusing on B. Still present is the assumption that B is complex (has high weight if measured in terms of symbol count). Of course, the program could get lucky, for example, in the case that B matched a resonator thus giving it a small weight (high priority for consideration). On the other hand, the fact that B is given a clause number of 20,000 matters not to the researcher; instead, what matters to the researcher is its close proximity to A, that of being an immediate child, causing it to be given preference through inheriting the importance given to A. That aspect of inherited importance is lost for the reasoning program; that B is the child of a key lemma, A, is in no way used by the program.

Thus, what might have appeared of little practical significance--the inclusion of a key lemma compared with the adjunction of that lemma--is shown to have possibly dire consequences. Yes, the use of the resonance strategy saves the day for the lemma itself, but has no effect on its progeny (except by accidental resonator matching). And yes, the addition of reliance on the ratio strategy helps a bit (by enabling the program to focus on some clauses based solely on first-come first-served), but often not enough.

Future Research

Based on the preceding observations, I am currently exploring a class of strategies based on th e notion of inheritance. The idea is to provide the reasoning program with the ability to capitalize on the ancestry of its conclusions, without the need for iteration and manual adjunction (in the input of a later run) of key lemmas that have been proved in a previous run. (I find it piquant that the set of support strategy--one of the first strategies I ever proposed--is an example of the use of inherited characteristics, in the sense that if at least one of the parents of a conclusion has support, so does the conclusion.)

References

[McCune1992] "Experiments in Automated Deduction with Condensed Detachment", Proceedings of the 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 607, ed. D. Kapur, Springer-Verlag, Berlin, 1992, pp. 209-223.

[Wos1995] Wos, L., "The Resonance Strategy", Computers and Mathematics with Application s 29, no. 2, 133-178 (February 1995).

Release 2.2.1 of the TPTP (Thousands of Problems for Theorem Provers) Problem Library is now available from the Department of Computer Science, James Cook University, Australia. It may be obtained either by anonymous FTP from

ftp.cs.jcu.edu.au:pub/research/tptp-library

or

As outgoing President of CADE Inc., I feel that this community needs an extended discussion of the state of the discipline as well as the structure, content, style, and purpose of CADE itself, including its relationship with cognate conferences and workshops. The annual business meeting is not, in my view, an adequate forum for such a discussion: perhaps a moderated newsgroup would be appropriate, since the issues are quite complex and widely divergent views are strongly held concerning them. I would personally be willing to do whatever CADE may feel is best to facilitate a community-wide discussion.

Finally, I hope it is in order for me to offer my personal congratulations to Bob Boyer and J Moore on their Herbrand Award. The award is for ``distinguished contributions" to automated deduction, which sums it up nicely. By their achievement and their example they have influenced the field deeply -- perhaps more so than we know.

Robert Boyer and J Strother Moore were awarded the Herbrand prize at CADE-16 in July 1999. The award was given to Drs. Boyer and Moore for their work on the automation of inductive inference and its application to the verification of hardware and software.

TABLEAUX 2000, "Automated Reasoning with Analytic Tableaux and Related Methods," will take place at the University of St Andrews, St Andrews, Scotland, on July 4-7, 2000.

The conference will include contributed papers, tutorials, system descriptions, a poster session, and invited lectures. Submissions are invited in four categories: A -- original research papers (up to 15 pages), B -- original papers on system descriptions (up to 5 pages), C -- experimental papers for the comparison of theorem provers, and D -- tutorials. Topics include the following:

The deadline for paper submissions (Categories A, B, and D) is December 1, 1999. Authors are requested to submit the papers via email in PostScript to the Program Chair (rd@dcs.st-and.ac.uk). The proceedings will again be published in Springer's LNAI series.

Entries for Category C will be reviewd by a small team led by Fabio Massacci of Universita` di Siena, who is organizing TANCS (TABLEAUX Comparison of Non-Classical Systems). Comparison entries should be sent to the Comparison Chair (tancs@dis.uniroma1.it) by January 19, 2000.