NEWSLETTER

No. 44, September 1999

**Table of Contents**

From the AAR President

The Power of Combining Resonance, Heat, and Hints

Lemma Inclusion vs Lemma Adjunction

New Release of TPTP Problem Library

CADE Inc. News

Updated AAR Membership List

Herbrand Award

Calls for Papers

The two main articles in this issue of the *AAR Newsletter* reflect some recent work that my colleague Branden Fitelson and I have been doing.
The article by Fitelson introduces a hybrid methodology that combines hints, resonance, and the hot list to find elegant proofs.
My article on lemma inclusion vs lemma adjunction discusses why the choice between these two may be crucial to the success of a reasoning program.

I encourage AAR members to try Fitelson's approach and to attempt to formulate yet other strategies. As you know, I strongly believe that the key to automated problem solving lies in more powerful strategies.

I also strongly encourage people to be sure to vote for the new CADE candidates for the CADE board of trustees. Your vote is important!

Over the past several years, Larry Wos has developed a powerful array
of techniques for finding elegant proofs [5]. These
methods have been implemented via clever uses of several Otter
strategies, including the *resonance strategy*
[3], the *hot list strategy* [2], and
various combinations of the two [6].

As the title of this note suggests, I will be discussing an extension
of some of Wos's methods for finding elegant proofs. This
extension--which has proved useful in several recent Otter
experiments--involves the addition of Bob Veroff's *hints
strategy* [1] into Wos's potent mixture of Otter
strategies. Specifically, I will describe two ways in which Veroff's
hints can usefully augment Wos's Otter arsenal for finding elegant
proofs.

Without getting into the details of Wos's techniques, I would like to
provide a brief, high-level overview of how the methodology works.
Basically, Wos [5] uses the following *iterative*
(but far from mechanical!) procedure:

- 1.
- Find an Otter proof (of some desired theorem ).
- 2.
- Place the proof steps
of
into
a
`weight_list`(typically,

`pick_and_purge`), assigning each*resonator*a low weight (typically,`2`). - 3.
- Place copies of some (or all) members of
`list(sos)`into`list(hot)`. - 4.
- Place some key lemmas
*that you believe will be proved during the next Otter run*into`weight_list(pick_and_purge)`with even lower weights (typically,`1`), and assign the parameter`dynamic_heat_weight`this same value, so that any formulas matching the*resonators*of those key lemmas will be*dynamically*adjoined to the hot list, once they are proven.^{1} - 5.
- Make "elegantizing" adjustments to other relevant Otter
parameters.
^{2} - 6.
- Rerun Otter, yielding (one hopes!) a more elegant proof of .
- 7.
- Repeat steps 1-6, until you reach a
*fixed point*Otter proof of , which can be made no more elegant by applying steps 1-6.

This (nonalgorithmic) technique has proved quite useful for finding elegant proofs, both in equational and nonequational first-order problems [4,5]. In the next section, I will explain how adding Veroff's hints strategy to this iterative methodology can serve to bolster its performance.

In step 2
of the methodology, we place the proof-steps
of our best-known Otter proof
of
into a
`weight_list` and assign each a weight of `2`. This
has the effect of telling Otter to assign any formula that matches
the *resonator* of any member of
a weight of two.

In step 4
of the methodology, we (*i*) place key lemmas
into a `weight_list` and assign each a weight of `1`,
then (*ii*) set the `dynamic_heat_weight` to `1`.
This has the effect of dynamically adjoining any formula that matches
the *resonator* of any of the key lemmas to the hot list during
the next Otter run.

As explained in [3], the *resonator* of a formula
is the *functional pattern* that formula exhibits. For instance,
the *resonator* `i(*,*)` of the formula `i(x,x)`
matches *both* of the formulas `i(x,x)` *and*
`i(x,y)`, even though the former does *not* subsume the
latter (i.e., the latter is *logically stronger* than the
former). The fact that resonators can match such a wide (logical)
variety of formulas is often a blessing. Experimental results have
indicated that the kind of "search latitude" that resonators afford
can be very helpful for both finding and shortening Otter proofs
[3,4,5,6].

Sometimes, however, the fact that resonators can match such a wide
(logical) variety of formulas is not such a good thing. For instance,
as Wos [5, Tendency 6] notes, if too many formulas are
adjoined to the hot list during an Otter run, this can "bog down":
the program and significantly decrease its effectiveness in both
finding and elegantizing proofs.
Step 4 of the methodology
could lead to just such a decrease in effectiveness, if the resonators
of the key lemmas match too many formulas that will be proven in the
next Otter run. Another way in which resonators can cause problems
involves
step 2 of the methodology
Otter searches for
proofs involving paramodulation and demodulation tend to be very
sensitive to the order in which demodulations are performed. As a
result, Otter often *fails* to reproduce such proofs (or more
elegant cousins thereof), *even* when their proof steps are used
as *resonators* *and* the `max_weight` is set to the
same value as that of the resonators. In such cases, it often helps
to have a "tighter logical grip" on the search space than the
resonance strategy (alone) provides. This is where Veroff's
*hints* can come in handy.

Veroff's hints strategy is explained and illustrated with examples in
[1]. We needn't concern ourselves here with the
details of how hints work. The key to understanding how hints can
augment the iterative methodology described above is getting clear on
the distinction between *hints* and *resonators*.

Unlike resonators, hints only match formulas that *subsume* them
or that are *subsumed by* them (or both, depending on how
various Otter settings are adjusted^{3}). Basically, this means that using a set
of formulas *as hints* to guide an Otter search places stronger
(logical) constraints on the search than using the same set of
formulas *as resonators* would. As I explained abstractly in the
preceding section, this "tighter logical grip" on the search space
can sometimes improve the performance of the iterative methodology.
In the next section, I will briefly describe some experimental
exploitations of this phenomenon.

There are two kinds of cases for which Veroff's hints strategy has been shown experimentally to provide useful augmentation to the methodology:

- Cases where we wish to adjoin lemmas dynamically to the hot
list during a run
(step 4).
In such cases, using
resonators as a means to this end often "bogs down" the search
because
*too many*formulas (matching the abstract functional pattern of the resonator) are added to the hot list. By assigning the`equiv_hint_wt`parameter of each of the desired lemmas*as hints*the same value as the`dynamic_heat_weight`parameter, one can add*exactly*those lemmas to the hot list as they are deduced during a run.^{4}- This hints-based alternative to step 4 of the methodology has proved especially useful in equational problems. In several cases, using hints rather than resonators in this step of the process has aided in the discovery of shorter proofs than were previously obtained using the iterative methodology (to be reported in more detail elsewhere).

- Cases where we wish to be able to reduce the
`max_weight`of the search significantly*and*, at the same time, to guide the search in*some*way using the proof steps of a known proof. This has to do with step 2 of the methodology. Here, we use the steps of our best-known proof*as resonators*to guide the Otter search. The idea is that we want to find more elegant proofs "in the neighborhood" of our best-known proof. As I mentioned above, Otter often fails to find*any*proofs when (*i*) the proof steps of a paramodulation/demodulation proof are used as resonators, and (*ii*) the`max_weight`is reduced to the value we assigned to the resonators. In such cases, it often helps to use the proof steps of the known proof*both as resonators and as hints*. By doing so, we are still able to reduce the`max_weight`(which typically reduces the time/memory each iteration through the methodology takes)*and*to more tightly constrain the search (which typically increases the probability that*some*proof will be found).- This
*hybrid*hints/resonators alternative to step 2 of the methodology has on several occasions aided in the discovery of shorter proofs than were previously obtained using the iterative methodology (to be reported in more detail elsewhere).

- This

Larry Wos's combination of resonance and heat has led to some very powerful iterative techniques for finding elegant proofs. But, there are certain potential shortcomings of resonance and heat, especially in the context of paramodulation/demodulation proofs. Because Veroff's hints strategy allows the Otter user to guard against some of these possible problems, it is a welcome addition to the growing Argonne methodology for finding elegant proofs.

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.

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?

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.

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.)

[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

Changes (from release v2.2.1) include the following:

- FOF problems
- 58 bugfixes done, in the domain SET
- 59 ratings changed
- CNF problems
- 3 bugfixes done, in the domain LAT
- 617 ratings changed

The TPTP is regularly updated with new problems, additional information, and enhanced utilities. Those who would like to register as a TPTP user and be kept informed of such developments should send e-mail to one of the following: Geoff Sutcliffe - geoff@cs.jcu.edu.au or Christian Suttner - suttner@informatik.tu-muenchen.de.

**New Secretary and New Elections Announced**

*Ulrich Furbach* (uli@informatik.uni-koblenz.de)

This year's election has to fill two open positions on the board of
trustees. As candidates we have
Harald Ganzinger,
Michael Kohlhase,
Neil Murray, and
David Plaisted. They will introduce themselves in the
*AAR Newsletter*. The election will be run by the secretary.

**President's Report -- July 1999**

*John Slaney* (John.Slaney@cisr.anu.edu.au)

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.

I am pleased to announce that after the last CADE (held in Trento, Italy, within FLOC99) the AAR has reached the level of 400 members. A new list of AAR members is available on the Web. If you have any corrections, please send them to bonacina@cs.uiowa.edu.

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.

Additional information is available from the FTP2000 Web site.

**Note:** The workshop will be held in conjunction with
* TABLEAUX 2000* (see below).

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.

For further details about the conference, see the Web site.