NEWSLETTER

From the AAR President

Call for Papers

CADE News: CADE-20

CADE News: Announcement of CADE Elections

TPTP Problem Library, Release v3.0.0

I am pleased to include in this issue a brief article by Lis Jump.
Lis and I worked together briefly; I taught her a bit about automated reasoning, and she proceeded to "beat the teacher" -- by finding a far shorter proof than I had found of a particular problem in group theory.
I encourage all of you now to try to "beat the student" or, better,
to send us equally challenging problems.
I firmly believe that such experimentation is the way to ever-more-powerful
automated reasoning programs.
(And then, you may announce your successes at one or more of the many
conferences and workshops announced in this issue of the
*AAR Newsletter.*

I have been studying automated reasoning with Dr. Larry Wos. As part of my studies, he suggested I revisit a problem from group theory that he had proven a few years ago. Wos used Otter to prove that Dr. Bill McCune's single axiom for groups of exponent 5 was indeed a single axiom. In short, the problem required that I prove

f(x,f(x,f(f(x,f(x,f(f(x,y),z))),f(e,f(z,f(z,f(z,z))))))) = yimplies

f(f(a,b),c) = f(a,f(b,c)) f(a,f(a,f(a,f(a,a)))) = e f(e,a) = a

with a single input file. Wos had originally obtained a 62-step forward proof of the above with no demodulation. I set out to use Otter to do something similar and in the process to learn more about automated reasoning.

Finding a forward proof of the theorem without using demodulation was nontrivial. Originally, I tried using Knuth-Bendix to find a proof and then eliminate demodulators individually, but had no success, so I started anew with a different tactic. First, I obtained a forward demodulation-free proof of the left identity. I added all of the steps of the proof to the hints list and moved left identity from the passive list to the set of support to create a different search space. Using this new search space, I achieved a forward proof of exponent five. I then eliminated the demodulators one at a time until the proof was demodulation free. I moved the steps of the new proof to the hints list and returned left identity from sos back to passive to obtain a forward proof of both left identity and exponent five with no demodulation. Finally, I replaced the current hints list with the hints generated from that proof and placed both left identity and exponent five in the set of support to try and obtain a proof of associativity. I proved associativity similarly, though it required a little more finesse. After this stage my proof was about 75 steps. This technique led me to a considerably different proof from the one obtained by Wos.

I then took my proof and attempted to shorten it. First, I took each step of the proof, individually, and demodulated it to junk so that it would not be available in the new proof. I considered all of the results and chose a few of the shortest, repeating the process until I was no longer obtaining shorter proofs. Then I had three different proofs, all about 68 steps long. Next, I experimented with various parameters for these proofs. I had the most success when I changed the backward subsumption hint weight from one to ten and set the order equations flag. This brought me a proof of 63 steps.

I took the 63-step proof and alternated between demodulating proof steps to junk and experimenting with various parameters. Using this method, I obtained a proof of 54 steps. Finally, at Wos's suggestion I placed the one axiom in the hot list, set heat to one, and repeated everything above. With this, I achieved a 51-step proof.

The final proof that I obtained had only sixteen steps in common with Wos's original 62-step proof. These include the three axioms required for the proof and the hypothesis.

Interested readers may examine the input file and proof , respectively.

**TIME 2005**

The 12th International Symposium on Temporal Representation and Reasoning will take place in Burlington, Vermont, June 23-25, 2005. Of interest is research on time-related problems within areas such as artificial intelligence, databases, and logic and computer-aided verification. Special emphasis is on new directions in time research. All submissions must be done electronically through the symposium Web page. The submission deadline is January 22, 2005.

The 12th international SPIN Workshop on Model Checking of Software will be held in San Francisco on August 22-24, 2005. SPIN 2005 solicits previously unpublished, currently unsubmitted, original contributions addressing theoretical, experimental and applied problems in model checking of software artifacts. Although authors are encouraged to compare their work with existing model checkers such as SPIN, the scope of the workshop is not limited to topics directly related to the SPIN system. Accepted contributions will be included in the workshop proceedings which will be published by Springer Verlag in the Lecture Notes in Computer Science series. The submission deadline: April 1 (abstracts) and April 8, 2005 (papers). For further information, see the Web site.

Topics of interest include the following:

- Combination of logics (e.g., modal logics, logics in AI)
- Combination of decision procedures, satisfiability procedures, and constraint solving techniques
- Combinations and modularity in term rewriting
- Integration of equational and other theories into deductive systems
- Combination of deduction systems and computer algebra
- Integration of data structures into CLP formalisms and deduction processes
- Model/problem analysis and decomposition
- Hybrid methods for deduction, resolution and constraint propagation
- Hybrid systems in computational linguistics, knowledge representation, natural language semantics, and human computer interaction
- Logical modeling of multi-agent systems
- Logical aspects of combining and modularizing programs and specifications

Submission categories include full papers, for work on foundations, applications, implementation techniques, and problem sets (up to 15 pages), as well as system descriptions (up to 8 pages), for describing publicly available systems. The submission deadline is May 2, 2005, for titles and abstracts, and May 9, 2005, for papers. For further information see the Web site.

The submission deadline is Feb. 13, 2005. Consult the Web for further details:

Authors are required to submit a paper title and a short abstract of about 100 words before submitting the extended abstract of the paper. All submissions must be electronic. Titles and short abstracts are due Jan. 5, 2005; extended abstracts are due Jan. 10, 2005. Authors will be notified of acceptance by March 18, 2005. Detailed information about electronic paper submission will be posted at the LICS Web site.

**Short Presentations:** LICS 2005 will have a session of short (5-10 minutes)
presentations. This session is intended for descriptions of work in
progress, student projects, and relevant research being published
elsewhere; other brief communications may be acceptable. Submissions for
these presentations, in the form of short abstracts (1 or 2 pages long),
should be entered at the LICS 2005 submission site March 19-25,
2005. Authors will be notified of acceptance or rejection by
April 1, 2005.

**Kleene Award for Best Student Paper:** An award in honor of the late
S. C. Kleene will be given for the best student paper, as judged by the
program committee. Details concerning eligibility criteria and procedure
for consideration for this award will be posted at the LICS website. The
program committee may decline to make the award or may split it among
several papers.

For detailed information see the Web site on workshops and on tutorials.

- Data structures and algorithms for the efficient representation of logical concepts
- Practical constraint handling
- Implementation of provers for different logics
- Efficient model generation
- Issues of reliability, witness generation, and witness verification
- Propositional logic (modulo theories) and decision procedures
- Implementation of higher-order logics and lambda-calculus
- Proof search organization and efficient heuristics for classical and inductive provers
- Experiences with new or unusual calculi
- Evaluation and benchmarking of provers and other logic-based systems
- System descriptions

Of especial interest are contributions that help the community understand how to build useful and powerful reasoning systems.

Researchers interested in participating are invited to send a short abstract (4-8 pages) to schulz@eprover.org by Jan. 14, 2005. Submissions should be in standard-conforming Postscript, PDF, or plain ASCII. Final versions will likely be required to be in Postscript or PDF and will be included in the proceedings. If possible, please use (PDF)LaTeX and the standard article class. Authors will be notified Feb. 11, 2005.

For information, see the Web page.

For more information and the technical details of the submission, see the Web page.

The 20th international Conference on Automated Deduction will take place in Tallinn, Estonia, July 22-27, 2005.

CADE is the major forum for the presentation of research in all aspects of automated deduction.

Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory.

Methods of interest include saturation, resolution, tableaux, sequent calculi, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, natural deduction, proof planning, proof presentation, proof checking, and explanation.

Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI.

Authors are invited to submit electronically (in postscript or PDF) full papers for work on foundations, applications or implementation techniques (15 pages), as well as system descriptions (5 pages) for describing publicly available systems. For further information and submission instructions, see the CADE-20 Web page.

**Deadlines:**

E-submission of title and abstract: February 25, 2005 E-submission papers: March 4, 2005 Notification of acceptance: April 22, 2005 Final version due: May 20, 2005

Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles Dowek (Ecole Polytechnique) and by Frank Wolter (U. Liverpool).

(Secretary of AAR and CADE)

E-mail: afelty@site.uottawa.ca

An election was held from September 23 through October 13 to fill
four positions on the board of trustees of CADE Inc. Maria Paola
Bonacina, David Basin, Gilles Dowek, Juergen Giesl, Rajeev Goré,
Hans de Nivelle, Geoff Sutcliffe, and Cesare Tinelli were nominated
for these positions. (See
*AAR Newsletter* No. 64, September
2004.)

Ballots were sent by electronic mail to all members of AAR on September 23rd, for a total of 630 ballots (up from 587 in 2003, 566 in 2002, 548 in 2001, 445 in 2000 and 396 in 1999). Of these, 125 were returned with a vote, representing a participation level of 19.8% (the same percentage exactly as in 2003, but down from 26.3% in 2002, 22.5% in 2001, 24.5% in 2000, and 30% in 1999). The majority is 50% of the votes plus 1, hence 63.

The following table reports the initial distribution of preferences among the candidates:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 30 | 22 | 22 | 15 | 3 | 0 | 2 | 31 | 125 |

D. Basin | 22 | 19 | 9 | 13 | 5 | 5 | 3 | 49 | 125 |

G. Dowek | 7 | 14 | 14 | 11 | 1 | 5 | 8 | 65 | 125 |

J. Giesl | 10 | 10 | 11 | 10 | 7 | 9 | 3 | 65 | 125 |

R. Goré | 15 | 18 | 17 | 13 | 3 | 4 | 0 | 55 | 125 |

H. de Nivelle | 7 | 11 | 16 | 17 | 4 | 7 | 8 | 55 | 125 |

G. Sutcliffe | 21 | 15 | 14 | 13 | 5 | 0 | 4 | 53 | 125 |

C. Tinelli | 13 | 13 | 15 | 15 | 9 | 4 | 4 | 52 | 125 |

No candidate reaches a majority right away. G. Dowek and H. de Nivelle have the same number of first preference votes, but Dowek is higher in the ranking because of receiving more second preference votes. The redistribution of the votes of H. de Nivelle yields the following new distribution:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 31 | 22 | 22 | 15 | 2 | 1 | 22 | 10 | 125 |

D. Basin | 23 | 19 | 13 | 10 | 6 | 5 | 26 | 23 | 125 |

G. Dowek | 7 | 15 | 17 | 7 | 4 | 9 | 34 | 32 | 125 |

J. Giesl | 11 | 12 | 12 | 7 | 12 | 5 | 30 | 36 | 125 |

R. Goré | 18 | 16 | 19 | 10 | 4 | 3 | 29 | 26 | 125 |

G. Sutcliffe | 21 | 22 | 13 | 10 | 2 | 4 | 29 | 24 | 125 |

C. Tinelli | 14 | 15 | 20 | 11 | 7 | 6 | 28 | 24 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 31 | 30 | 18 | 12 | 2 | 7 | 20 | 5 | 125 |

D. Basin | 24 | 21 | 15 | 7 | 8 | 12 | 24 | 14 | 125 |

J. Giesl | 13 | 10 | 13 | 13 | 9 | 13 | 34 | 20 | 125 |

R. Goré | 20 | 16 | 20 | 9 | 4 | 15 | 25 | 16 | 125 |

G. Sutcliffe | 23 | 22 | 15 | 8 | 3 | 18 | 24 | 12 | 125 |

C. Tinelli | 14 | 20 | 22 | 7 | 8 | 18 | 20 | 16 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 33 | 31 | 21 | 7 | 6 | 11 | 14 | 2 | 125 |

D. Basin | 27 | 21 | 16 | 8 | 11 | 11 | 23 | 8 | 125 |

R. Goré | 22 | 17 | 20 | 10 | 11 | 12 | 23 | 10 | 125 |

G. Sutcliffe | 25 | 23 | 13 | 10 | 15 | 13 | 19 | 7 | 125 |

C. Tinelli | 17 | 19 | 20 | 12 | 15 | 13 | 22 | 7 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 38 | 38 | 14 | 6 | 7 | 12 | 10 | 0 | 125 |

D. Basin | 30 | 23 | 18 | 8 | 8 | 23 | 13 | 2 | 125 |

R. Goré | 24 | 22 | 19 | 12 | 7 | 21 | 18 | 2 | 125 |

G. Sutcliffe | 29 | 22 | 14 | 17 | 10 | 17 | 13 | 3 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 46 | 42 | 6 | 5 | 13 | 8 | 5 | 0 | 125 |

D. Basin | 35 | 28 | 14 | 6 | 15 | 19 | 7 | 1 | 125 |

G. Sutcliffe | 36 | 21 | 23 | 6 | 17 | 11 | 10 | 1 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of D. Basin, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

M. P. Bonacina | 64 | 30 | 0 | 12 | 14 | 2 | 3 | 0 | 125 |

G. Sutcliffe | 44 | 36 | 1 | 12 | 21 | 7 | 3 | 1 | 125 |

M. P. Bonacina is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 30 | 18 | 10 | 10 | 4 | 4 | 35 | 14 | 125 |

G. Dowek | 11 | 17 | 16 | 3 | 5 | 8 | 45 | 20 | 125 |

J. Giesl | 13 | 11 | 12 | 12 | 9 | 3 | 50 | 15 | 125 |

R. Goré | 17 | 27 | 16 | 5 | 5 | 0 | 41 | 14 | 125 |

H. de Nivelle | 11 | 16 | 19 | 9 | 7 | 8 | 45 | 10 | 125 |

G. Sutcliffe | 29 | 11 | 17 | 11 | 0 | 4 | 36 | 17 | 125 |

C. Tinelli | 13 | 21 | 19 | 10 | 5 | 5 | 36 | 16 | 125 |

None of the candidates has a majority to be elected, so the votes of H. de Nivelle need to be redistributed again:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 32 | 17 | 15 | 6 | 6 | 15 | 31 | 3 | 125 |

G. Dowek | 11 | 21 | 13 | 5 | 9 | 19 | 42 | 5 | 125 |

J. Giesl | 15 | 12 | 13 | 14 | 5 | 20 | 41 | 5 | 125 |

R. Goré | 21 | 24 | 17 | 4 | 4 | 21 | 28 | 6 | 125 |

G. Sutcliffe | 31 | 16 | 17 | 4 | 4 | 18 | 29 | 6 | 125 |

C. Tinelli | 14 | 29 | 15 | 8 | 6 | 18 | 30 | 5 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 35 | 20 | 10 | 10 | 6 | 24 | 18 | 2 | 125 |

J. Giesl | 17 | 10 | 21 | 10 | 11 | 25 | 29 | 2 | 125 |

R. Goré | 24 | 25 | 14 | 6 | 12 | 20 | 21 | 3 | 125 |

G. Sutcliffe | 33 | 18 | 17 | 3 | 14 | 18 | 19 | 3 | 125 |

C. Tinelli | 15 | 37 | 11 | 6 | 16 | 14 | 24 | 2 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 38 | 23 | 13 | 3 | 20 | 19 | 8 | 1 | 125 |

J. Giesl | 20 | 15 | 22 | 8 | 20 | 25 | 15 | 0 | 125 |

R. Goré | 28 | 30 | 7 | 10 | 19 | 20 | 9 | 2 | 125 |

G. Sutcliffe | 37 | 21 | 10 | 12 | 16 | 17 | 10 | 2 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 45 | 23 | 9 | 6 | 22 | 15 | 5 | 0 | 125 |

R. Goré | 32 | 30 | 13 | 5 | 22 | 16 | 7 | 0 | 125 |

G. Sutcliffe | 40 | 21 | 19 | 6 | 18 | 14 | 7 | 0 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of R. Goré, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

D. Basin | 57 | 20 | 1 | 14 | 25 | 4 | 4 | 0 | 125 |

G. Sutcliffe | 49 | 31 | 1 | 15 | 17 | 7 | 5 | 0 | 125 |

Thus, D. Basin is elected to the board of trustees. (Since 57 votes does not suffice for the majority, the STV algorithm executes another round distributing the votes of G. Sutcliffe, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 18 | 16 | 11 | 6 | 8 | 24 | 35 | 7 | 125 |

J. Giesl | 16 | 12 | 16 | 10 | 6 | 27 | 32 | 6 | 125 |

R. Goré | 26 | 27 | 10 | 7 | 0 | 22 | 27 | 6 | 125 |

H. de Nivelle | 12 | 23 | 16 | 11 | 8 | 25 | 27 | 3 | 125 |

G. Sutcliffe | 32 | 16 | 17 | 3 | 4 | 25 | 20 | 8 | 125 |

C. Tinelli | 20 | 19 | 19 | 8 | 7 | 23 | 22 | 7 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 19 | 18 | 11 | 10 | 10 | 35 | 20 | 2 | 125 |

J. Giesl | 18 | 14 | 18 | 9 | 11 | 31 | 23 | 1 | 125 |

R. Goré | 30 | 24 | 12 | 4 | 9 | 29 | 15 | 2 | 125 |

G. Sutcliffe | 35 | 24 | 8 | 5 | 13 | 23 | 14 | 3 | 125 |

C. Tinelli | 22 | 26 | 16 | 7 | 12 | 25 | 16 | 1 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of J. Giesl, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 24 | 18 | 12 | 11 | 15 | 32 | 12 | 1 | 125 |

R. Goré | 35 | 23 | 12 | 5 | 14 | 27 | 8 | 1 | 125 |

G. Sutcliffe | 38 | 23 | 11 | 9 | 16 | 17 | 10 | 1 | 125 |

C. Tinelli | 25 | 25 | 19 | 10 | 15 | 22 | 9 | 0 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

R. Goré | 42 | 20 | 13 | 5 | 19 | 21 | 4 | 1 | 125 |

G. Sutcliffe | 43 | 26 | 12 | 5 | 19 | 16 | 3 | 1 | 125 |

C. Tinelli | 29 | 32 | 18 | 5 | 18 | 19 | 4 | 0 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of C. Tinelli, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

R. Goré | 50 | 25 | 0 | 14 | 26 | 6 | 4 | 0 | 125 |

G. Sutcliffe | 52 | 28 | 1 | 14 | 22 | 4 | 4 | 0 | 125 |

Thus, G. Sutcliffe is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 22 | 16 | 11 | 7 | 18 | 32 | 16 | 3 | 125 |

J. Giesl | 20 | 15 | 13 | 12 | 15 | 34 | 14 | 2 | 125 |

R. Goré | 33 | 27 | 9 | 1 | 13 | 26 | 12 | 4 | 125 |

H. de Nivelle | 19 | 23 | 13 | 10 | 18 | 30 | 9 | 3 | 125 |

C. Tinelli | 29 | 19 | 16 | 9 | 12 | 24 | 13 | 3 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of H. de Nivelle, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 24 | 18 | 12 | 12 | 21 | 32 | 4 | 2 | 125 |

J. Giesl | 23 | 18 | 15 | 10 | 24 | 26 | 8 | 1 | 125 |

R. Goré | 38 | 25 | 6 | 7 | 20 | 21 | 6 | 2 | 125 |

C. Tinelli | 35 | 23 | 12 | 9 | 18 | 20 | 7 | 1 | 125 |

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

G. Dowek | 30 | 18 | 17 | 4 | 34 | 18 | 3 | 1 | 125 |

R. Goré | 45 | 23 | 7 | 4 | 28 | 14 | 3 | 1 | 125 |

C. Tinelli | 39 | 24 | 15 | 5 | 27 | 10 | 5 | 0 | 125 |

Again, no candidate reaches a majority, and by redistributing the votes of G. Dowek, one gets the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
6rd pref. |
7th pref. |
8th pref. |
Total |

R. Goré | 54 | 21 | 0 | 14 | 26 | 7 | 2 | 1 | 125 |

C. Tinelli | 48 | 30 | 1 | 13 | 25 | 5 | 3 | 0 | 125 |

Thus, R. Goré is elected to the board of trustees.

After this election, the following people are serving on the board of trustees of CADE Inc.:

Franz Baader (President, CADE-19 Program Chair, elected 10/2003)

David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)

Peter Baumgartner (elected 10/2003)

Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)

Amy Felty (Secretary, appointed 5/2004)

Rajeev Goré (elected 10/2004)

Michael Kohlhase (elected 10/2000, reelected 10/2003)

Neil Murray (Treasurer)

Robert Nieuwenhuis (CADE-20 Program Chair)

Geoff Sutcliffe (elected 10/2004)

Andrei Voronkov (Vice President, CADE-18 Program Chair, elected 10/2002)

Toby Walsh (elected 10/2002)

On behalf of the AAR and CADE Inc., I thank Frank Pfenning for his service as trustee and CADE Inc. president during the past 6 years, Gilles Dowek and John Harrison for their service as trustees during the past three years, all candidates for running in the election, all the members who voted; and offer congratulations to David Basin, Maria Paola Bonacina, Rajeev Goré, and Geoff Sutcliffe on being elected, and to Franz Baader on being elected president of CADE Inc.

Dept. of Computer Science, University of Miami, USA

geoff@cs.miami.edu

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

TPTP v3.0.0 is now available on the Web. The TPTP-v3.0.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online.

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 email Geoff Sutcliffe.

**What's New in TPTP v3.0.0**

Changes from v2.7.0 to v3.0.0 for FOF problems

- new abstract problems
- new problems
- new generators
- 53 bugfixes done, in the domains AGT SYN
- ratings changed

Changes from v2.7.0 to v3.0.0 for CNF problems

- new abstract problems
- new problems
- new generators
- 1 bugfix done, in the domains SWC
- ratings changed

The library has been translated to the new TPTP syntax (aka the TSTP syntax).

- The BNF for the new TPTP syntax has been added to the Documents directory.
- Equality is now written in infix, using = and !=
- CNF ``conjecture"s have been changed to ``negated_conjecture"
- $true and $false are now reserved constants and have been used as expected.

Equality is now assumed to be built in, and all equality axioms have been removed from all problems.

Problem status values have been updated to the SZS problem status ontology:

- The ontology has been added to the Documents directory.
- FOF problems with conjectures are one of Theorem, CounterSatisfiable, Unknown, Open.
- FOF problems without conjectures are one of Unsatisfiable, Satisfiable, Unknown, Open.
- CNF problems are one of Unsatisfiable, Satisfiable, Unknown, Open.

tptp1T has been updated to understand the new status values.

No numbers appear in any problems--numbers are now reserved for future built-in treatment.

The tptp2X utility has been extended and improved:

- The new TPTP syntax (aka the TSTP syntax) is the default output format
- The old TPTP syntax is available as the oldtptp format
- rm_equality with no selection removes all
- add_equality has been parameterized like rm_equality
- New set_equality transform
- New prefix format
- FOF files with multiple conjecture formulae are expanded to multiple files each with a single conjecture and all the other formulae.
- Searches for include files:
- No search for absolute names
- Relative names are searched for under the $TPTP environment variable and if not found then under the current working directory

- Explicit support for YAP Prolog
- Installation is done by editing the *.uninstalled files and creating the final files. This solves some CVS problems.

Gail W. Pieper

pieper@mcs.anl.gov

December 2004