NEWSLETTER

No. 45, October 1999

**Table of Contents**

From the AAR President

Results of the CADE Trustee Elections

Calls for Papers

New Book

This issue follows quickly on the last one, principally because we wished to announce the results of the CADE election of officers. We have also included calls for papers and demos, as well as an announcement of a contest for ATP systems.

If the rate of progress in automated reasoning follows the pattern of the past decade, the next millenium should be most rewarding!

(Secretary of AAR and CADE)

E-mail: bonacina@cs.uiowa.edu

The 1999 CADE Trustee elections were held from September 17 through October 17. Ballots were sent by electronic mail to all members of AAR as of September 17, for a total of 396 ballots. Of these, 119 were returned with a vote, representing a participation level of 30%. The majority is 50% of the votes plus 1, hence 60.

The following table reports the distribution of preferences:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
Total |

Harald Ganzinger | 49 | 20 | 16 | 34 | 119 |

Michael Kohlhase | 24 | 25 | 19 | 51 | 119 |

Neil V. Murray | 21 | 15 | 15 | 68 | 119 |

David A. Plaisted | 25 | 47 | 8 | 39 | 119 |

No candidate reaches a majority right away, and since Neil Murray turns out to be the weakest candidate by a few votes, his votes are redistributed, yielding the following new distribution:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
Total |

Harald Ganzinger | 55 | 25 | 20 | 19 | 119 |

Michael Kohlhase | 31 | 27 | 33 | 28 | 119 |

David A. Plaisted | 31 | 45 | 31 | 12 | 119 |

Again, no candidate reaches a majority, and Michael Kohlhase turns out to be the second weakest candidate, because the tie with David Plaisted in the count of the first preferences is broken by the difference in the second preferences. The redistribution of his votes yields the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
Total |

Harald Ganzinger | 70 | 25 | 19 | 5 | 119 |

David A. Plaisted | 40 | 61 | 17 | 1 | 119 |

At this point, Harald Ganzinger has a majority and is elected. His votes are redistributed, producing the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
Total |

Michael Kohlhase | 31 | 25 | 43 | 10 | 119 |

Neil Murray | 29 | 18 | 53 | 19 | 119 |

David Plaisted | 58 | 21 | 31 | 9 | 119 |

None of the candidates has a majority to be elected, so that votes need to be redistributed again. The weakest candidate is again Neil Murray by a few votes, so that his votes are redistributed as follows:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
Total |

Michael Kohlhase | 45 | 40 | 29 | 5 | 119 |

David Plaisted | 67 | 35 | 13 | 4 | 119 |

At this point, David Plaisted has a majority and is elected.

On behalf of the AAR and CADE communities, congratulations to Harald and David on being elected, many thanks to Michael and Neil for running, and thanks to all those who voted.

For further information, see the Web site.

Submissions are solicited in two categories:

The submission deadline for both types of paper is January 15, 2000.For further information, see the Web site.

The last three streams effectively constitute the former ICLP conference series that will be now integrated into CL2000. ILP2000 will be collocating as a separate conference.

Papers on all aspects of the theory, implementation, and application of computational logic are invited. The deadline for submissions is February 1, 2000.

For further information, see the Web site.

For further information, see the Web site.

New benchmarks also will be available for converse propositional dynamic logic.

Submissions are invited as original, unpublished experimental papers describing a theorem prover and its performance on the benchmarks of the TANCS 2000 Comparison. Beside the paper, entrants are requested to submit the executable (or source code) of their prover and a summary of the experimental data upon which their paper is based. The experimental papers, together with information on the comparison design and results, will appear in the proceedings of the TABLEAUX-2000 conference published by Springer Verlag in the LNAI series. The deadline for submission is January 19, 2000.

The comparison of the submitted systems will be mainly based on two aspects: (1) effectiveness, measured by the type and number of problems solved, the average runtime for successful solutions the scaling of the prover as problems get bigger; and (2) usability, measured by the availability of the prover via Web or other sources the portability of the code to various platforms the ease of installation and use

For further information, see the Web site.

For further information, see the Web site.

**Contents**

Introduction - M. Fitting

Tableau Methods for Classical Proposaitional Logic - M. D'Agostino

First-order Tableau Methods - R. Letz
Equality and Other Theories - B. Beckert

Tableaux for Intuitionsitic Logics - A. Waaler and L. Wallen

Tableau Methods for Modal and Temporal Logics - R. Gore'

Tableau Methods for Substructural Logics - M. D'Agostino, D. Gabbay, K. Broda

Tableaux for Nonmonotonic Logics - N. Olivetti

Tableaux for Many-Valued Logics - R. Hahnle

Implementing Semantic Tableaux - J. Possegga and P. Schmitt

A Bibliography on Analytic Tableaux Theorem Proving - G. Wrightson

Index