Included in this issue of the AAR Newsletter is an update on the TPTP Problem Library. This release (or a patch) will be used in the CADE-16 ATP System Competition. As those familiar with me know, I am in favor of such contests, not because I am competitive, but because these contests can stimulate the development of more powerful automated reasoning programs. My compliments to Geoff Sutcliffe and Christian Sutner for their continued efforts.

Also included in this issue are two announcements about the Herbrand Award. I firmly believe that such awards, particularly when they are highly publicized, can bring honor to our field. I congratulate Gerard Huet, and I encourage AAR members to submit nominations of worthy candidates.

Announcement of the 1998 Herbrand Award

Gerard Huet was awarded the Herbrand prize at CADE-15 in July 1998. The award was given to Dr. Huet in honor of his contributions to term rewriting and to theorem proving in higher-order logic, as well as many other contributions to the field of automated reasoning.

Call for Nominations for Future Herbrand Awards

The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE meeting. Whether and to whom an award will be given is decided by the CADE Trustees, the current CADE Program Committee, and previous recipients of the award.

The Herbrand Award has been given in the past to Larry Wos (1992), Woody Bledsoe (1994), Alan Robinson (1996), Wu Wen-Tsun (1997), and Gerard Huet (1998).

A nomination is required for consideration for the Herbrand award. Nominations can be made at any time and remain open indefinitely, but only nominations received by 16 April 1999 will be considered for a Herbrand Award at CADE-16 in July 1999.

Nominations should consist of a letter (preferably e-mail) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders.

Call for Nominations

The board of trustees of the Conference on Automated Deduction Inc. (CADE) have created an award in honor of the memory of Woody Bledsoe for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students.

CADE-16 will take place in Trento, Italy. The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP system development, and to expose ATP systems to interested researchers, an ATP system competition (CASC-16) will be held at CADE-16 on Friday, July 9, 1999.

CASC-16 will evaluate the performance of sound, fully automatic, first-order ATP systems. The evaluation will be in terms of the number of problems solved and the average runtime for successful solutions, in the context of

• a bounded number of eligible problems, chosen from the TPTP Problem Library, and
• a specified time limit for each solution attempt.

The competition organizers are Geoff Sutcliffe and Christian Suttner. The competition will be overseen by a panel of knowledgeable researchers who are not participating in the event. The competition will be run on computers provided by SUN Germany.

The TPTP Problem Library, Release v2.2.0
Geoff Sutcliffe (geoff@cs.jcu.edu.au) and
Christian Suttner (suttner@informatik.tu-muenchen.de)

The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with

• A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism.
• A comprehensive list of references and other interesting information for each problem.
• New generalized variants of problems whose original presentation is hand- tailored towards a particular automated proof.
• Arbitrary size instances of generic problems (e.g., the N-queens problem).
• A utility to convert the problems to existing ATP systems' formats.
• General guidelines outlining the requirements for ATP system evaluation.

The principal motivation for this project is to move the testing and evaluation of ATP systems from the previously ad hoc situation onto a firm footing. This became necessary, as results being published do not always accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.

TPTP v2.2.0 is now available from the Department of Computer Science, James Cook University, Australia. It may be obtained either by anonymous FTP from

Here is a full (I think) bibliography of my work on instance-based theorem proving methods. The idea of instance-based theorem proving is to show that a set S of first-order clauses is unsatisfiable by constructing a set T of ground instances of clauses in S and testing T for unsatisfiability using an efficient propositional decision procedure. This bibliography includes not only my own works, but several other papers by others which it turns out are closely related. In all, there are over 30 papers. Most of these are co-authored by me. Though this approach may not be as well known as others, it is noteworthy that instance-based theorem proving methods often far outperform other strategies, even when implemented in Prolog. In addition to these references, another paper of mine about the use of this approach for set theory problems is forthcoming, and instance-based theorem proving also far outperforms resolution for certain set theory problems, without any human guidance. Finally, I have developed another extension of clause linking which has not been written up, which should have significant advantages on many applications.

A survey of our work on instance-based approaches, written about 1996:

The following two letters were submitted by D. Plaisted in response to the recent CADE election.

Unanswered Questions - David A. Plaisted, January 24, 1999

I wish to express some concerns about the conduct of the 1998 CADE trustee election. Because this election is a matter affecting the entire CADE community, the particulars need to be widely known.

Based on the information I have, I narrowly missed being elected as a trustee, with over 80 votes cast. But for me, that is the least of my complaints. What concerns me much more is the conduct of the election, and even more the failure of the trustees to answer my questions about the conduct of the election. My questions began even before knowing the results of the election. It would only take a couple of minutes for the trustees to respond to me.

Let me give some background to this situation. At CADE 98, three people, including myself, were nominated for two trustee positions. At the time, there was a discussion about making AAR membership free. Instead of just getting the election over with the current membership, a discussion was held between the trustees and AAR about membership qualifications, and due to this and other delays the election was held about three months after CADE (and later than the time limit allowed by the bylaws). I had asked to be informed of the date of the election, but never was.

It was eventually decided that AAR membership should be free. This system has its advantages, but a problem with this is that someone could swing an election just by having 20 of his friends sign up for AAR membership and vote for him.

In the preceding trustee election, brief biographies of the candidates were e-mailed to all voters. I supplied such a biography for the 1998 election, but it was not used; instead, a web link was given, which not many people accessed. It is much better to mail out biographies, as many people are unaware of the career histories of the candidates.

The ballot was sent out with two lists of names in different orders. The first was Kirchner, Pfenning, Plaisted and the second was Kirchner, Plaisted, Pfenning. I can't imagine why the CADE secretary would list the names in two different orders, which can only promote confusion.

There were no acknowledgments of ballots, so there was no guarantee that ballots were not simply dropped without a trace. (I grant that this is unlikely.) In addition, the initial plan was to use a vote counting program to tally the votes, which was a concern to me, not knowing how well it was tested.

Even more frustrating was the fact that my questions, after a while, were ignored. Especially were my questions about the mechanism for storing ballots met with silence. If the election software stores the names of voters with ballots, then acknowledgments could be sent out and duplicate votes detected. If not, then there is no safeguard against multiple votes by one person. The trustees have refused to answer my questions about this. If the ballots are just stored with numbers in place of names, then having two lists of voters is a tremendous opportunity for trouble in matching up numbers with names.

Another issue is verifying that only AAR members voted, which is impossible unless names are stored with ballots.

I sent in several suggestions about how to acknowledge the votes, which were ignored. Finally (on Friday the 13th, no less), I got a terse message about the results of the election. My suggestions never were even acknowledged.

If I did something to offend the trustees so that they refuse to answer me, I apologize. But I am not aware of what this could be.

Let the trustees print out a list of e-mail addresses of the voters, if they can. The we can at least check if the list is correct, and if the number of addresses equals the listed number of votes.

The trustees could at least say, We think every single member of AAR is too honest to vote more than once, or, We goofed, we are very sorry, but it would be too much trouble to do the election over, or whatever. I realize that we all make mistakes. But not to get any response at all is unacceptable.

I can't imagine what would motivate the trustees to ignore my questions. Did I annoy the president of CADE? Was he embarrassed that the election was poorly run, and too embarrassed to respond? Did the CADE secretary simply rebel and refuse to send out acknowledgments? Was the election rigged? Were the trustees too busy with other matters, and didn't think my questions mattered? Were the trustees angry at me? Why couldn't they take two minutes to answer my questions?

I would hate to think that the trustees would consider that it is not worth answering someone who represents less than some percentage of the CADE community. Are only the winners of elections worth consideration?

I don't think you can imagine the feelings that I experienced as a result of my questions to the trustees being stonewalled. It is enough to make me never want to attend another CADE conference in my life. This is perplexing to me, since I have confidence in a number of the trustees, and cannot imagine what is going on.

I also requested to see the ballots after the election (with names removed), but never did.

My confidence in the trustees was shaken by having to fight to get a democratic system installed, and then only achieving a compromise, partially democratic system, with the trustees still not showing much interest in making it more democratic. Now there are problems with this election, and my questions go unanswered.

The conduct of elections is at the heart of a democratic system, so a mismanaged election is a serious matter, even if all candidates are qualified. If the trustees can convince me that this election is OK, I am glad to listen.

I sent a message to the theorem proving list proposing a simple and verifiable mechanism for conducting elections. The idea is to post the ballots, identified by time stamps, and post the list of voters. This way everyone can verify that their name is listed if and only if they voted, that the number of ballots is equal to the number of voters, and that their ballot appears with the proper time stamp. In my posting to the theorem proving list, I requested that the trustees adopt this scheme, but received no response. I also repeated my questions about the trustee election, but received no response. In addition, I requested that original ballots be recovered and acknowledgments be sent out, but this request was also ignored.

The current system is also deficient in that the CADE secretary, who counts the ballots, may have preferences among the candidates. Either a verifiable election system should be instituted, or the ballots should be counted by an independent agency.

The trustees could at least have everyone resend their votes for this election to a different person who can recount them, to make sure there were no duplicate or dropped votes.

As you can see, there are quite a few problems with the current election, which is unfortunate for me, since this may be the only trustee election I will ever participate in.

A couple of trustees say that we should concentrate on improving future elections, and just accept the result of this one. But why can we not at least know the truth about this one? In the future, if there are problems, the trustees can again say, we will fix it later, and thus we can have a string of problem elections without any being corrected.

As one who had a lot to do with the establishment of the current (partially) democratic system, and as a candidate, I think I have a right to know what is going on. If the election results can be trusted, I got nearly half of the over 80 second round votes cast. This also indicates a substantial level of support within the CADE community.

One trustee suggested to me that an election could be held to decide on a new election mechanism. The time stamp mechanism I proposed in my message to the theorem proving list is simple and verifiable, and should not need a vote to be instituted. If scheme B is more verifiable than scheme A, and only 10 percent of the voters want scheme B, then why not use it, as it doesn't disadvantage the other 90 percent of the voters at all?

If you are concerned about the conduct of this election, or the failure of the trustees to answer my questions, or if you favor instituting a verifiable election mechanism, please send me e mail at plaisted@cs.unc.edu. Your name will be kept confidential.

I also want to correct a statement in an article in the January 1999 issue of the AAR Newsletter. The article by John Slaney about the 1998 CADE trustee election states that the CADE secretary of the trustees has an unlimited term. This is incorrect. According to my understanding of the bylaws, the CADE secretary is appointed for three year terms by the trustees.

Questions Still Unanswered - David A. Plaisted, February 14, 1999

The CADE trustees recently (February 10) sent me an e-mail response to an earlier draft of my AAR Newsletter article concerning the CADE election. I am grateful to finally receive a response, though it would have helped to have it much earlier. I wish to respond in turn.

I do find it encouraging that the trustees are planning to improve the election mechanism in the future.

Unfortunately, the trustees' response never did answer my most pressing question, which concerns the election mechanism. They never did say how the election software processed the ballots, and how they were internally represented. Why not? Were the voters' names stored with the ballots, or not? And how did they verify that no one voted more than once?

The trustees state

The secretary verified manually that none of the votes sent to his mailbox were overlooked. According to his check, no duplicate votes were counted.

This seems to state that no votes were overlooked. However, the election software decided what was a ballot. If it did not recognize something as a ballot, it was sent to the CADE secretary's mailbox. Otherwise, the ballot was subject to some mysterious processing whose details never have been made public. So the trustees' above statement appears only to be referring to the small portion of the votes that were not recognized by the software, and not to the great majority of them. Thus it seems possible that the above statement of the trustees says quite the opposite of what it appears to say.

Such verbal dodgery (if it is so) can only fuel speculation that there is something seriously wrong with this election which the trustees are attempting to hide.

There are a number of other problems with their response. For example, they say that they cannot print out a list of the voters, as that is not permitted in a secret ballot. This is false, as printing out lists of voters is common in secret ballots conducted by e-mail. I wonder if the reason that a list of names was not published is that the trustees could not do it, rather than that they did not see it as necessary.

The trustees said they did not see a need to send out acknowledgments during the election. I don't see why it would have been hard to do this manually. It would only have meant sending out about 84 replies by hand. Or if they had explained the election mechanism more clearly (which they still have not done), I would see why acknowledgments were not needed. The CADE president did explain in an earlier message to me (October 14 1998) why it was unlikely for ballots to be lost in the mail, but did not explain the safeguards against someone voting twice. My response was that sending out acknowledgments would increase reliability, and there was no reason not to do it. Acknowledgments could be sent out even now if the names really are stored with the ballots, as would be necessary for the CADE secretary to verify no duplicate ballots as it was claimed that he did.

The October 14 message also did not explain how the ballots were represented, which could be important to know with two lists of candidates in different orders. If the candidates are represented by numbers rather than names, then the vote count may reveal that candidates 1 and 2 have won. Depending on which list of candidates one uses, this could be a different set of winners.

The trustees did not explain why the lists of names appeared in two orders on the ballot (which may indeed have a reasonable explanation), nor did they respond to my request to see the ballots with voter names deleted. They also did not say why I was not informed of the date of the election in advance, as I had requested; I assume that was just an oversight.

The trustees stated that no one has ever complained about the election procedure before. But 10 to 15 individuals so far have sent me e-mail expressing sympathy with my election concerns. One of them even said that it was hopeless to get the trustees to be reasonable, and I should just give up.

In sum, what is the situation?

1. The trustees simply will not mail out acknowledgments, even though it would only take a short time to do so even now.

2. The trustees simply will not explain the details of the election mechanism, even though this was my most pressing question to them.

3. The trustees simply will not print out the list of e-mail addresses of those who voted, even though it would take only a small amount of time, and not violate a secret ballot.

4. For a long time, the trustees simply would not respond to my questions.

I consider this behavior inappropriate. The function of leaders should be servants, not lords, even to those whom they consider to be troublemakers and pests, if that is what I am considered. And why am I in this controversy? Only for requesting what is reasonable and fair. When I ran the FTP election, I would have bent over backwards to satisfy such requests, especially from a candidate.

There are also a number of minor problems with their response.

The trustees said that some of my questions about the STV procedure did not merit replies. This point is not relevant, as I sent in a couple of questions, and then in the next hour or so realized my error and sent in a message to that effect to the trustees. No one would imagine that those previous questions were still on my mind, so I cannot understand why this was even brought up. Further, it is not so that these questions were not worth answering. This is a complicated election procedure, and a candidate's questions about it certainly are worth answering.

The trustees said I alleged misconduct. I did not state this, but did find the failure to respond to my questions earlier inexcusable. I realize that we all have time pressures, but at least some response about the election mechanism could have been made much earlier.

The trustees said that by being a candidate, I implicitly agreed to the election being conducted in the usual manner, and so should not complain. The usual manner for me includes acknowledgments. And if the usual manner needs improvement, it should be done, without using my ``implicit agreement'' as an excuse.

It is not necessarily so easy to detect someone trying to swing an election by having his friends join the AAR, as the trustees claim, since membership is free, but this is a minor point.

I did not state that the failure to mail out biographies was misconduct. But for someone who is undecided, it could be the difference between voting and not voting. However, this is a minor issue.