NEWSLETTER
No. 45, October 1999
Table of Contents
From the AAR President
Results of the CADE Trustee Elections
Calls for Papers
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!
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:
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:
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:
At this point, Harald Ganzinger has a majority and is elected.
His votes are redistributed, producing the following table:
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:
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.
CADE-17
The 17th International Conference on Automated Deduction
will take place June 17-20, 2000, in Pittsburgh, Pennsylvania.
Original research papers (15 pages)
are solicited
in all aspects of automated theorem proving, automated reasoning, computer aided
verification, formal methods, and static analysis.
Systems descriptions (5 pages) are also solicited;
system description submissions must include a
URL for a Web page from which the system can either be run
or obtained by reviewers.
Both types of papers will be published in the
proceedings of CADE-17 by Springer-Verlag.
The deadline for submission is January 15, 2000.
Proposals are also solicited for workshops (June 21) and tutorials
(June 16).
Anyone wishing to organize such an event should send (e-mail preferred) a
proposal no longer than two pages to the workshop chair
Michael Kohlhase (kohlhase@cs.uni-sb.de)
by November 30, 1999.
The proposal should describe the
topic of the proposed workshop or tutorial and explain why the topic is relevant to CADE.
Recent CADE workshops have included term schematizations and their applications, reasoning, automation of proofs
by induction, empirical studies in logic algorithms, mechanization of partial functions, proof search in type-theoretic
languages, automated model building, evaluation of automated theorem-proving systems, strategies in automated
deduction, automated theorem proving in software engineering and in mathematics and integration of symbolic computation
and deduction. Workshops may have the same topic as those of previous workshops, and this practice is encouraged.
Recent CADE tutorials have included equality reasoning in semantic tableaux, proof systems for nonmonotonic logics,
rewrite techniques in theorem proving, proof planning, parallelization of deduction strategies, resolution decision
methods, constructive type theory, the use of semantics in Herbrand-based proof procedures, logical frameworks,
theorem proving by the inverse method, deduction methods based on Boolean rings, higher-order equational logic, and
term indexing in automated reasoning.
For further information, see the
Web site.
CAV 2000
The 12th Conference on Computer Aided Verification will take place in
Chicago, Illinois, on July 15-19, 2000.
The CAV 2000 conference is the twelfth in a series dedicated to the
advancement of the theory and practice of computer-assisted formal
analysis methods for software and hardware systems. The conference
covers the spectrum from theoretical results to concrete
applications, with an emphasis on practical verification tools and
the algorithms and techniques that are needed for their
implementation.
The proceedings of the conference will be published
in the Springer-Verlag Lecture Notes in Computer Science series.
Topics include modeling and specification formalisms, algorithms and tools,
verification techniques, applications and case studies, testing
based on verification technology, and verification in practice.
Submissions are solicited in two categories:
For further information, see the
Web site.
CL 2000
The international conference on Computational Lagoic
(CL 2000)
will take place at
Imperial College, London, UK, July 24-28, 2000.
CL2000 is the first conference in a major new series of annual
international conferences bringing together the various communities
of researchers who have a common interest in computational logic.
CL2000 is collocating with three conferences:
DOOD2000: 6th Int'l Conference on Rules and Objects in Databases;
ILP2000: 10th Int'l Workshop on Inductive Logic Programming; and
LOPSTR2000: 10th Int'l Workshop on Logic-based Program Synthesis
and Transformation.
CL2000 will include seven streams covering various subfields of
computational logic, each with its own separate program committee:
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.
FTP'2000
FTP'2000 is the third in a series of workshops focusing
on first-order theorem proving as a core theme of automated
deduction and providing a forum for presentation of recent
work and discussion of research in progress.
The workshop will be held in conjunction with TABLEAUX 2000
at St Andrews, Scotland, on July 3-5, 2000.
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;
and implementation techniques and applications of first-order theorem
provers to problems in verification, artificial intelligence, and
mathematics.
Authors are invited to submit papers in the following
categories: (1) extended abstracts of 5-8 pages describing original
results not published elsewhere, (2) position papers of 1-2 pages
describing the author's research interests in the field, work in
progress, and future directions of research, and (3) practical contributions
of 1-5 pages consisting of new problem sets, system descriptions, or
solution processes to problem sets.
System demonstrations will be possible.
Submission deadline for all papers is April 2, 2000.
For further information, see the
Web site.
TANCS 2000
The Tableaux Non-Classical Systems Comparison will take place
at the 7th International Conference on Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX)
at St Andrews, Scotland, July 4-7, 2000.
The TABLEAUX conferences are a major forum for the presentation of
new research in all aspects of automated deduction. In order to
stimulate automated theorem proving and satisfiability testing
development in nonclassical logics, and to expose ATP systems to
interested researchers, the TANC Systems Comparison will be held at
TABLEAUX-00.
The aim of TANCS is to compare the performance of fully
automatic, non-classical ATP systems (based on tableaux, resolution,
rewriting, etc.) in an experimental setting and promote the
experimental study on theorem proving and satisfiability testing in
non-classical logics.
For TANCS-2000 the focus is on extended modal and description logics.
In particular, benchmarks derived from combinatorial problems
will be available for
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.
CSL 2000
The annual conference of the
European Association for Computer Science Logic
will take place at Fischbachau/Munich, Germany, on August 21-26, 2000.
The conference is intended for computer scientists
whose research activities involve logic, as well as for logicians working
on issues significant for computer science.
Topics of interest include
automated deduction and interactive theorem proving,
categorical logic and topological semantics,
type theory,
equational logic and term rewriting,
higher-order logic,
logic programming, constraints,
modal and temporal logics, and
program specification, transformation, and verification.
Submitted papers
(not to exceed 15 pages)
must arrive by January 31, 2000.
Papers accepted by the Program Committee must be presented at the
conference and will appear in a proceedings volume, to be published by
Springer-Verlag in the LNCS series.
For further information, see the
Web site.
From the AAR President, Larry Wos...
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
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
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
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
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
Michael Kohlhase
45
40
29
5
119
David Plaisted
67
35
13
4
119
The submission deadline for both types of paper is
January 15, 2000.