No. 43 March 1999

Table of Contents

From the AAR President
News from the AAR Secretary
Announcement of the 1998 Herbrand Award
CADE Woody Bledsoe Student Travel Award
Call for Papers:

  • Third International Tbilisi Symposium on Language, Logic and Computation
  • LPAR'99
  • ICLP'99

  • The CADE-16 ATP System Competition
    The TPTP Library
    Bibliography of Instance-Based Theorem Proving
    CADE Election Revisited

    From the AAR President, Larry Wos...

    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.

    News from the AAR Secretary:
    AAR Member List on the World Wide Web

    Maria Paola Bonacina
    Dept. of Computer Science - The University of Iowa

    The AAR Newsletter used to publish periodically the list of all AAR members; with the Newsletter on the World Wide Web this service has been replaced by a list of members on the Web reachable from the AAR home page and directly at the Web site

    I encourage all members to visit this new page at the AAR site, and send me by e-mail the URL of their home page, if missing. The list of members on the Web will be updated at least once per year and as time permits.

    Herbrand Award

    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.

    CADE Woody Bledsoe Student Travel Award

    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.

    The award is intended to cover much of the expense for a small number of students working in the field of automated deduction to attend CADE-16 to be held in Trento, on July 7-10, 1999 (see the Web site). The winners will be reimbursed (to a maximum of USD 600) for his or her conference registration, transportation, and accomodation expenses.

    Preference will be given to students who will be playing an active role in the conference, including the attached workshops, and to students who do not have alternative funding.

    Nominations, which should include a recommendation of up to 300 words from the student's supervisor, should be sent by e-mail to

    with copies to and

    Nominations must arrive no later than April 30, 1999, and the winner(s) will be notified by May 15. 1999. The award will be presented at CADE-16; in case a winner does not attend, the trustees may transfer the award to another nominee or give no award.

    Harald Ganzinger, CADE-16 PC Chair


    John Slaney, President of Trustees, CADE, Inc.

    Call for Papers

    Third International Tbilisi Symposium on Language, Logic and Computation
    (see the
    Web site)

    The Tbilisi International Symposium on Language, Logic and Computation will be held at Batumi September 12-16, 1999. The Symposium welcomes papers on current research in all aspects of linguistics, logic, and computation, including automated reasoning, logic programming, constructive logic, and modal systems. Papers concerning applications of logic to computation and the application of logic and computation to language description and modeling are strongly encouraged.

    Abstracts (2000 words) of submissions should be submitted by e-mail to no later than April 15, 1999. The collection volume of the short versions will be available during the symposium. The proceedings with full papers are planned immediately after the symposium.

    In parallel with the symposium, three tutorials will be given by outstanding scholars for students and post-graduates. These tutorials are explicitly meant to address interdisciplinary issues in the fields of logic and language, algebraic logic, and computation and morphology.

    The symposium will be immediately preceded by the Conference on Logical Programming and Automatic Reasoning (see below).

    (see the
    Web site)

    The Conference on Logical Programming and Automatic Reasoning will take place in Tbilisi, Republic of Georgia, September 6-10, 1999. Topics include all forms of logic, automated reasoning, formal methods, knowledge representation and reasoning, rewriting, logic programming, constraints, and finite model theory.

    Details on submission procedures can be found at the LPAR'99 Web site.

    (see the
    Web site)

    The International Conference on Logic Programming will take place on November 29 - December 4, 1999, at Las Cruces, New Mexico. Papers are sought in all areas of logic programming including theory, implementation, and application. Abstracts must be received by May 4, 1999. Details on submission procedures can be found at the ICLP'99 Web site.

    The CADE-16 ATP System Competition

    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

    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.

    Further details and registration information are available at the Web site. System registration for CASC-16 closes on June 7, 1999.

    The TPTP Library

    The TPTP Problem Library, Release v2.2.0
    Geoff Sutcliffe ( and
    Christian Suttner (

    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

    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

    or from
    one or the other Web sites.

    Instructions for fetching and unpacking the TPTP are given below in the Quick Guide. There are three files in the TPTP distribution: ReadMe-v2.2.0, TPTP-v2.2.0.tar.gz, and General information about the library is in the ReadMe-v2.2.0 file, the library is packaged in TPTP-v2.2.0.tar.gz, and a technical report describing the TPTP (in postscript form) is in Please read the ReadMe file, as it contains up-to-date information about the TPTP. The technical report serves as a manual explaining the structure and use of the TPTP. It also explains much of the reasoning behind the development of the TPTP.

    The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please e-mail one of us.

    What's New in TPTP v2.2.0

    TPTP v2.2.0 contains 4004 problems in 28 domains. Changes (after v2.1.0) are

    Tools for the TPTP Problem Library
    Geoff Sutcliffe (

    The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. Since its first release 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation.

    Two new tools for accessing and using the TPTP have recently been developed. They are

    The TPTP, these new tools, and other useful TPTP related material, are available from one or the other TPTP WWW pages.

    Bibliography of Instance-Based Theorem Proving

    David A. Plaisted (

    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:

    Plaisted, D., The Use of Semantics in Instance-Based Proof Procedures, available on the Web.

    The basic method of clause linking without semantics:

    Inference by clause matching, with Shie-Jue Lee, in Intelligent Systems, Z. Ras and M. Zemankova, eds. (Ellis Horwood, New York, 1990), pp. 200 - 235.

    We show that it is better than resolution and other methods on near propositional problems and logic puzzles:

    Eliminating duplication with the hyper-linking strategy, with Shie-Jue Lee, Journal of Automated Reasoning 9:1 (1992) 25-42.

    A general paper about clause linking without semantics:

    Theorem proving using hyper-matching strategy, with Shie-Jue Lee, International Symposium on Methodologies for Intelligent Systems, October, 1989, Charlotte, North Carolina, also appeared in Methodologies for Intelligent Systems 4, Z. Ras, ed. (North-Holland, 1989), pp. 467-476.

    The model finding part of clause linking without semantics:

    New applications of a fast propositional calculus decision procedure, with Shie-Jue Lee, Proceedings of the 8th Biennial Conference of Canadian Society for Computational Studies of Intelligence, (CSCSI-90), University of Ottawa, Ottawa, Ontario, CANADA, May 23-25, 1990, pp. 204-211.

    The use of replacement rules with clause linking:

    Reasoning with predicate replacement, with Shie-Jue Lee, International Symposium on Methodologies for Intelligent Systems, Knoxville, Tennessee, October 24 - 26, 1990; also appeared in Methodologies for Intelligent Systems 5, Z. Ras, M. Zemankova, and M. Emrich, eds. (North-Holland, 1990), pp. 530 - 537.

    A way to find some proofs faster in instance-based theorem proving using unit resolution:

    Searching for small proofs in automatic theorem proving, with Shie-Jue Lee, Proceedings of National Computer Symposium, Chung-Li, Taiwan, Dec. 18-19, 1991, pages 626-632.

    Some refinements of clause linking:

    Use of Unit Clauses and Clause Splitting in Automatic Deduction, with Shie-Jue Lee, Proceedings for the 4th International Conference on Computing and Information, Toronto, Ontario, Canada, May 28-30, 1992, pages 228-232. Editors: W.W. Koczkodaj, P.E. Lauer, and A.A. Toptsis. IEEE Computer Society Press.

    An extension of clause linking to equality (which didn't work very well) based on Brand's modification method:

    Proving equality theorems with hyper-linking, with Geoff Alexander, system abstract, Eleventh International Conference on Automated Deduction, Saratoga Springs, New York, June 16 - 18, 1992.

    An invited survey of the work on clause linking with and without semantics and its relation to conditional term-rewriting systems:

    Conditional term rewriting and first-order theorem proving, invited talk, with Geoff Alexander, Heng Chu, and Shie-Jue Lee, Third International Workshop on Conditional Term-Rewriting Systems, Pont-à-Mousson, France, July 8-10, 1992, to appear in the final proceedings.

    Replacement rules with clause linking, which (with some guidance) vastly outperforms resolution on many set theory and temporal logic problems:

    Use of replace rules in theorem proving, with Shie-Jue Lee, Methods of Logic in Computer Science 1 (1994) 217-240.

    Using instance based theorem proving to solve logic puzzles by constructing models:

    Problem solving by searching for models with a theorem prover, with Shie-Jue Lee, Artificial Intelligence 69 (1994) 205-233.

    Clause linking with semantics, which obtains some reasonably hard theorems:

    Model Finding Strategies in Semantically Guided Instance-Based Theorem Proving, with Heng Chu, International Symposium on Methodologies for Intelligent Systems (ISMIS '93), June 15-18, 1993, Norway. Proceedings to be published by Springer-Verlag in Lecture Notes in Artificial Intelligence. See also:

    Model finding in semantically guided instance-based theorem proving, with Heng Chu, Fundamenta Informaticae 21:3 (1994) 221 - 235.

    Clause linking with semantics, combined with a kind of resolution to eliminate large literals:

    Rough Resolution: A Refinement of Resolution to Remove Large Literals, with Heng Chu, Eleventh National Conference on Artificial Intelligence, Washington, DC, July 11 to July 16, 1993.

    A method of using specialized decision procedures (constraints) and incorporating semantics with clause linking:

    Use of Presburger Formulae in Semantically Guided Theorem Proving, with Heng Chu, Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, January 2-5, 1994. (No proceedings.)

    The basic idea of semantic hyper-linking, an extension of clause linking to use semantic information:

    Semantically Guided First-Order Theorem Proving using Hyper-Linking, with Heng Chu, Twelfth Conference on Automated Deduction, Nancy, France, June 28 - July 1, 1994.

    A search strategy for use with instance based theorem proving that controls the consumption of storage:

    Controlling the consumption of storage with sliding priority search in a hyper-linking based theorem prover, with Shie-Jue Lee, Computers and Artificial Intelligence 14:6 (1995) 563-578.

    A brief overview of clause linking with semantics:

    CLINS-S: A Semantically Guided First-Order Theorem Prover, with Heng Chu, JAR 18(2).

    A brief overview of The RRTP theorem prover, another instance-based theorem prover based on replacement rules:

    M. Paramasivam and David A. Plaisted, RRTP, A Replacement Rule Theorem Prover, Journal of Automated Reasoning, 18(2) pp. 221-226, 1997.

    A paper mostly about efficiency of propositional decision procedures, which also has some information about clause linking:

    Propositional Search Efficiency and First-Order Theorem Proving, with Geoffrey D. Alexander, Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11-13, 1996), Ding-Zhu Du, Jun Gu, and Panos Pardalos, eds., (AMS, 1997, Providence, RI), pp. 335-350.

    The RRTP theorem prover and its performance on an application (description logics), where it often outperforms specialized methods:

    M. Paramasivam and David A. Plaisted, Automated Deduction Techniques for Classification in Description Logics, Journal of Automated Reasoning 20(3), June, 1998, pp. 337-364.

    An introduction to ordered semantic hyper-linking (OSHL), another instance-based strategy which uses semantics and also has an efficient equality mechanism:

    Plaisted, D. and Yunshan Zhu, Ordered Semantic Hyper Linking, Proceedings of Fourteenth National Conference on Artificial Intelligence (AAAI97), July 27 - 31, 1997, Providence, Rhode Island

    A more detailed paper about OSHL:

    D. Plaisted and Y. Zhu, Ordered Semantic Hyper-Linking, Journal of Automated Reasoning, to appear.

    A book giving an asymptotic analysis of the complexity of many theorem proving strategies, including some instance-based ones:

    The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis (Vieweg, Wiesbaden, 1997), 170 pp, with Yunshan Zhu.

    The application of OSHL to planning problems, where it outperforms resolution:

    FOLPLAN: A Semantically Guided First-Order Planner, with Yunshan Zhu, 10th International FLAIRS Conference, Daytona Beach, Florida, May 11-14,1997.

    Another theorem proving strategy closely related to clause linking, it turns out, but developed independently:

    A partial instantiation based first-order theorem prover, by Hooker, Rago, Chandru, and Shrivastava, in Proceedings of the Second International Workshop on First-order Theorem Proving (FTP), Schloss Wilhelminenberg, Vienna, Austria, November 1998. Technical Report E1852-GS-981, Technische Universität Wien, 106-115, 1998.

    A previous method on which Hooker's work is based:

    Jeroslow, R.G., Computation-oriented reductions of predicate to propositional logic, Decision Support Systems 4 (1988) 183-197.

    A very early instance-based method:

    Gilmore, P. C., A Proof Method for Quantification Theory, IBM Journal of Research and Development 4 (1960) 28-35.

    An early method with some similarities to clause linking:

    Davis, M., Eliminating the Irrelevant from Mechanical Proofs, Proceedings Symp. of Applied Math, vol. 15, pp. 15-30, 1963.

    The basis of the well-known Davis and Putnam procedure used in many instance-based methods:

    Davis, M. and Putnam, H., A Computing Procedure for Quantification Theory, JACM 7 (1960) 201-215.

    A modification of Davis and Putnam's method which is commonly used today:

    Davis, M., Logemann, G. and Loveland, D., A Machine Program for Theorem-Proving, CACM 5 (1962) 394-397.

    CADE Election Revisited

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