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

  • New Secretary and New Elections Announced
  • President's Report - July 1999
    Updated AAR Membership List

    Herbrand Award
    Calls for Papers
  • FTP2000
  • TABLEAUX 2000

    From the AAR President, Larry Wos...

    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!

    The Power of Combining Resonance, Heat, and Hints
    Branden Fitelson (


    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.

    A Brief Overview of Wos's Methodology

    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:

    Find an Otter proof (of some desired theorem ).
      Place the proof steps of into a weight_list (typically,
    pick_and_purge), assigning each resonator a low weight (typically, 2).
    Place copies of some (or all) members of list(sos) into list(hot).
      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
    Make "elegantizing" adjustments to other relevant Otter parameters.2
    Rerun Otter, yielding (one hopes!) a more elegant proof of .
    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.

    Two Potential Problems Involving Resonators

    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.

    How Veroff's Hints Can Help

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

    Experimental Applications

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


    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.


    Thanks to Larry Wos for many useful and stimulating conversations during the past year about automated reasoning (and life).


    1 R. Veroff. Using hints to increase the effectiveness of an automated reasoning program: Case studies. Journal of Automated Reasoning, 16(3):223-239, 1996.

    2 L. Wos with Gail Pieper. The hot list strategy. Journal of Automated Reasoning, 22(1):1-44, 1999.

    3 L. Wos. The resonance strategy. Computers and Mathematics with Applications, 29(2):133-178, 1995.

    4 L. Wos. The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial. Academic Press, 1996.

    5 L. Wos. Automating the search for elegant proofs. Journal of Automated Reasoning, 21(2):135-175, 1998.

    6 L. Wos. The power of combining resonance with heat. Journal of Automated Reasoning, 17(1):23-81, 1998.

    Lemma Inclusion versus Lemma Adjunction
    Larry Wos (

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


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

    New Release of the TPTP Problem Library
    Geoff Sutcliffe (
    Christian Suttner (

    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


    the Web.

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

    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 - or Christian Suttner -

    CADE Inc. News

    New Secretary and New Elections Announced
    Ulrich Furbach (

    John Slaney's term on the board of trustees expired. He was since CADE-16 President of CADE Inc. The CADE community appreciates very much his service. The president's report is contained in this newsletter.

    The new secretary of CADE Inc. is Maria Paola Bonacina. According to the bylaws she is an ex officio member of the board of trustees. Welcome, Maria Paola! Many thanks to Neil Murray, who served the previous years as secretary. Neil continues to serve as treasurer of CADE Inc., and he is proposed as a candidate for the upcoming elections for the board of trustees.

    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 (

    The final budget of CADE-15 was duly received and showed a surplus. The Trustees wish to express once again their thanks to Wolfgang Bibel and his conference committee, to Claude and Helene Kirchner and to their program committee for organizing a successful CADE last year in Lindau.

    The election of trustees took place, somewhat delayed by difficulties over determining exactly who is a member of CADE and eligible to vote. The result of the ballot was very close, Claude Kirchner and Frank Pfenning being duly elected. As a result of concerns raised by David Plaisted, the Trustees have agreed to review the mechanism for processing votes in time for the next election. In particular, it should be possible for voters to receive email confirmation that their vote has been registered.

    It is pleasing to note that we were able to provide student bursaries (the "Bledsoe Awards") to a greater number of people than ever before. The Trustees hope and expect that this tradition will continue in future CADEs.

    During the year there was much discussion of moves to counter the perceived fragmentation of our field.

  • The First International Conference on Computational Logic, CL2000, will take place in London next year and will include an automated deduction stream along with six others. The Trustees did not take a position on this initiative: as individuals, some of us welcomed this initiative, but we felt that CADE should remain separate from CL at least for the present. Any future FLoC would need to be timed so as not to be in opposition to any future CL.
  • In a separate development, Joerg Siekmann and others have raised the idea of an International Federation of Computational Logic. The Trustees are supportive of this Federation, but as yet there is no formal link between it and CADE.
  • 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.

    Updated Membership List of the Association for Automated Reasoning
    Maria Paola Bonacina

    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

    Herbrand Award

    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.

    Calls for Papers


    The third international workshop on First-order Theorem Proving will be held on July 3-5, 2000, at the University of St Andrews, St Andrews, Scotland.

    FTP2000 provides a forum for presentation of very recent work and discussion of research in progress. The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, and modal logics, including resolution, equational reasoning, term rewriting, model construction, constraint reasoning, unification, propositional logic, specialized decision procedures; strategies and complexity of theorem-proving procedures; implementation techniques; and applications of first-order theorem provers to problems in verification, artificial intelligence, and mathematics.

    The workshop will include discussion of problem sets, provided both by the organizers and by the participants. Discussion of a problem set will include its significance, difficulty, history, and solutions or solution attempts. Real-world problems are especially welcome.

    Authors are invited to submit papers in three categories: (1) extended abstracts (5-8 pages) describing original results not published elsewhere; (2) position papers (1-2 pages) describing the author's research interests in the field, work in progress, and future directions of research; and (3) practical contributions (1-5 pages) consisting of new problem sets, system descriptions, or solution processes to problem sets according to the guidelines above. System demonstrations will be possible. Submissions should be sent by e-mail in Postscript format to by April 2, 2000. Authors of accepted papers are expected to present their contribution at the workshop.

    Accepted submissions will be collected in a volume to be distributed at the workshop. Additionally, the submissions will be made available on the Web after the workshop. Authors will be invited to submit a full version, which will again be refereed. The selected papers will be published in the workshop proceedings.

    Additional information is available from the FTP2000 Web site.

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

    TABLEAUX 2000

    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:

  • analytic tableaux for various logics (theory and applications)
  • related techniques and concepts, e.g., model checking and BDDs
  • related methods (model elimination, sequent calculi, connection method, etc.)
  • new calculi and methods for theorem proving in classical and non-classical logics (modal, description, intuitionistic, linear, temporal, etc.)
  • systems, tools, implementations and applications (e.g., verification)
  • 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 ( 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 ( by January 19, 2000.

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