NEWSLETTER
From the AAR President
I join Maria Paola in congratulating the new CADE trustees.
And I am pleased to see that membership in CADE continues to increase.
I would, however, like to see all our members contributing
articles, problems, challenges---not only to the AAR Newsletter but
also to the Journal of Automated Reasoning.
Yes, I do mean "all": if we have to expand the journal
and run more issues of the newsletter, marvelous.
While I am making outrageous requests, let me add the following.
Please flood me with information about how you are using OTTER:
in education, program verification, protocol analysis---whatever.
An election was held from September 26 through
October 15, 2003, to fill three positions on the board
of trustees of CADE Inc.
The three positions were left vacant by
Ulrich Furbach, Michael Kohlhase, and David McAllester,
whose terms expired.
Franz Baader, Peter Baumgartner, Michael Kohlhase, and Stephan Schulz
were nominated for these positions
(see AAR Newsletter No. 60, September 2003).
Michael Kohlhase was nominated for a second term;
Franz Baader was nominated for a first term as elected trustee,
after one year as CADE 2003 Program Chair;
and Peter Baumgartner and Stephan Schulz were nominated for a first term.
Ballots were sent by electronic mail to all members
of AAR as of September 26,
for a total of 587 ballots (up from 566 in 2002,
548 in 2001, 445 in 2000, and 396 in 1999).
Of these, 116 were returned with a vote, representing a participation
level of 19.8% (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 59.
The following table reports the initial distribution of preferences
among the candidates:
No candidate reaches a majority right away,
and the redistribution of the votes of Stephan Schulz
yields the following new distribution:
Again, no candidate reaches a majority, and
by redistributing the votes of Michael Kohlhase one gets the following table:
Thus, Franz Baader has a majority of preferences and
is elected for a first term as elected trustee.
The redistribution of the votes of the winner
produces the following table:
Peter Baumgartner has a majority right away and is elected.
Redistributing Peter Baumgartner's votes,
one obtains the following matrix:
There is a majority of preferences for
Michael Kohlhase, who is elected.
In the weeks following the elections,
the Board of Trustees elected Frank Pfenning and
Andrei Voronkov as
president and vice-president, respectively, of CADE Inc.,
resulting in the following list of CADE Trustees:
Franz Baader (Past program chair, elected 10/2003)
On behalf of the AAR and CADE Inc.,
I thank Ulrich Furbach, for his service as trustee and CADE Inc. president
during the past six years;
David McAllester, for his service as trustee during the past three years;
Stephan Schulz, for running in the election;
and all the members who voted, for their participation;
and I offer the warmest congratulations to Franz Baader, Peter Baumgartner,
and Michael Kohlhase on being elected trustees
and to Frank Pfenning and Andrei Voronkov on being elected president and
vice-president, respectively, of CADE Inc.
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 or IJCAR meeting.
The Herbrand Award has been given in the past to
Larry Wos (1992)
A nomination is required for consideration for the Herbrand award.
The deadline for nominations for the Herbrand Award that will be
given at IJCAR 2004 is
Nominations should consist of a letter (preferably email) 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. Nominations should be sent to
The International Joint Conference on Automated Reasoning
(IJCAR 2004)
will take place July 4-8, 2004, in Cork, Ireland.
This second IJCAR will merge CADE, FTP,
TABLEAUX, FroCoS (Workshop on Frontiers of Combining Systems), and
CALCULEMUS (Symposium on the Integration of Symbolic Computation and
Mechanized Reasoning).
Tutorials for IJCAR 2004
will be held on July 4-5, 2004. They may run a half-day or full day.
An IJCAR tutorial can be on any IJCAR-related topic. (Examples of
IJCAR areas of interest can be found in the IJCAR Call for Papers at
the
Web.) The following kinds of
tutorials are especially desirable:
A tutorial that explains how to use a particular automated
reasoning system to an audience of future users.
Interested readers should sent
a two- to three-page proposal to the tutorial chair (wmfarmer@mcmaster.ca)
no later than February 1, 2004. The proposal should be in plain text,
postscript, or PDF format and should contain the following
information:
Title of the tutorial.
Tutorial participants are not required to register for IJCAR
2004.
Tutorial organizers must, however, create and maintain a Web page that
describes the tutorial for the IJCAR community.
The IJCAR organizers offer to copy and distribute tutorial
notes to registered tutorial participants.
All questions concerning tutorials should be directed to the
tutorial chair
William Farmer
(wmfarmer@mcmaster.ca).
RTA'04
The 15th International Conference on Rewriting Techniques and Applications (RTA'04)
will be held June 3-5, 2004, as
part of the Federated Conference on Rewriting, Deduction and
Programming (RDP'04).
RTA is the major forum for the presentation of research on all aspects
of rewriting.
Typical areas of interest include
the following:
Invited talks will be given at RTA'04 by
Neil Jones (Copenhagen),
Aart Middeldorp (Innsbruck), and
Robin Milner (Cambridge).
Interested researchers are
invited to submit a paper. The deadlines are
January 15, 2004, for electronic submission of title and short abstract,
and
January 22, 2004, for electronic submission of the full paper.
Submissions must be original and not submitted for publication
elsewhere.
Submission categories include regular research
papers and system descriptions. Problem sets and
submissions describing interesting applications of rewriting
techniques are also welcome.
Accepted papers will appear in the Springer-Verlag
Lecture Notes in Computer Science series. More information about
paper submission will be available at the RDP'04
Web.
A 1000 Euro award will be given to the best paper or papers as decided
by the program committee. The award may also totally or partially go to the best
paper with a student as main author, according to the submission letter.
For further details please contact the program chair:
AISC 2004
The Seventh International Conference on
Artificial Intelligence and Symbolic Computation
will take place
September 22-24, 2004,
at the
Research Institute for Symbolic Computation,
Castle of Hagenberg, Austria.
Artificial intelligence and symbolic computation are two views and approaches
for automating problem solving,
in particular mathematical problem solving.
The two approaches are based on heuristics and on mathematical algorithmics,
respectively.
Artificial intelligence can be applied to symbolic computation and
vice versa; hence,
a wealth of challenges, ideas, theoretical insights and results,
methods, and algorithms arise in the interaction of the two fields and research communities.
Advanced tools of software technology and system design are needed, and a broad spectrum of applications is possible by the combined problem solving power of the two fields.
Researchers working in
artificial intelligence,
symbolic computation,
computer algebra,
automated theorem proving,
and automated reasoning are invited
to share their views, work, and results by submitting papers and participating in the conference.
Papers should be submitted by May 1, 2004.
The proceedings of the conference containing the refereed and accepted papers will appear as a volume of the Springer-Verlag Lecture Notes.
For details see
the
Web.
WoLLIC'2004
The 11th Workshop on Logic, Language, Information and Computation
will take place
in Paris
July 19-22, 2004.
The aim of the workshop is to foster interdisciplinary research in pure and
applied logic.
Contributions are invited in the form of short papers (12 A4 10pt pages) in
all areas related to logic, language, information, and computation.
The papers should be sent
preferably in postscript format by
e-mail to wollic@cin.ufpe.br.
Submissions must be received by
one of the co-chairs of the organizing committee by March 1, 2004.
Papers must be anonymous: A separate identification page must be included.
The papers must be
written in English and give enough detail to allow the program committee
to assess the merits of the work. Papers should start with a brief
statement of the issues, a summary of the main results, and a statement
of their significance and relevance to the workshop. References and
comparisons with related work are also expected. Technical development
directed to the specialist should follow. Results must be unpublished
and not submitted for publication elsewhere, including the proceedings
of other symposia or workshops. One author of each accepted paper will be
expected to attend the conference in order to present the paper. Authors will be
notified of acceptance by April 1, 2004.
The proceedings will appear as a volume in the Elsevier series
Electronic
Notes in Theoretical Computer Science.
Full versions of papers will be refereed again for publication in a special
issue of the Logic Journal of the IGPL.
ASL sponsorship of WoLLIC'2004 also will permit student ASL members to
apply for (limited)
ASL travel funds that we hope to make available for
sponsored meetings that take place in 2004
In addition, WoLLIC'2004 will make available modest grants to
graduate students in logic and to recent Ph.D.'s so that they may attend the
meeting in Paris.
To be considered for a grant, please (1) send a letter of application, and
(2) ask your thesis supervisor to send a brief recommendation letter.
The application letter should be brief (one page) and should include
(1) your name, (2) your home institution, (3) your thesis supervisor's name,
(4) a one-paragraph description of your studies and work in logic,
(5) your estimate of the travel expenses you will incur,
(6) (for citizens or residents of EU) citizenship or visa status, and
(7) (voluntary) indication of your gender and minority status. Only modest
grants will be possible, partially covering travel costs and perhaps some of
the living expenses during the meeting. Women and members of minority groups
are strongly encouraged to apply.
Application by e-mail is encouraged; put "WoLLIC grant application"
in the subject line of your message. Applications and recommendations should
be received before the deadline of March 1, 2004, by one of the co-chairs
of the organizing committee.
For further information,
contact one of the co-chairs of the organizing committee:
Patrick Cegielski
Ruy de Queiroz
Or, see the
Web.
Reasoning about Uncertainty, by
Joseph Y. Halpern
Uncertainty is a fundamental and unavoidable feature of daily life; in order
to deal with uncertainty intelligently, we need to be able to represent it
and reason about it. In this book Joseph Halpern examines formal ways of
representing uncertainty and considers various logics for reasoning about
it. While the ideas presented are formalized in terms of definitions and
theorems, the emphasis is on the philosophy of representing and reasoning
about uncertainty; the material is accessible and relevant to researchers
and students in many fields, including computer science, artificial
intelligence, economics (particularly game theory), mathematics, philosophy,
and statistics.
Halpern begins by surveying possible formal systems for representing
uncertainty, including probability measures, possibility measures, and
plausibility measures. He considers the updating of beliefs based on
changing information and the relation to Bayes' theorem; this leads to a
discussion of qualitative, quantitative, and plausibilistic Bayesian
networks. He considers not only the uncertainty of a single agent but also
uncertainty in a multiagent framework.
Halpern then considers the formal logical systems for reasoning about
uncertainty. He discusses knowledge and belief; default reasoning and the
semantics of default; reasoning about counterfactuals, and combining
probability and counterfactuals; belief revision; first-order modal logic;
and statistics and beliefs. He includes a series of exercises at the end of
each chapter.
456 pp., cloth, ISBN 0-262-08320-5, US$50
Automated Reasoning and the Discovery of Missing and Elegant Proofs
This book is rare--perhaps the only one of its type--in that it
simultaneously provides the basis for diverse courses in logic, mathematics,
and automated reasoning; teaches how research can be successfully conducted;
and presents results that had eluded various masters for many decades.
Key to obtaining these results is the use of strategies and methodologies,
detailed in this volume, and the program OTTER--which
automates logical reasoning, deducing millions of conclusions that follow
inevitably from the hypotheses supplied by the user.
In this book, various aspects of the newly discovered Hilbert's twenty-fourth
problem are addressed.
The included CD-ROM offers OTTER in various forms, numerous input files, and a
large number of proofs that are new.
By experimenting with these offerings, both the new researcher and the expert
alike may experience the excitement of attacking deep open questions and
discovering missing and elegant proofs.
384 pp., with CD-ROM, hardcover, ISBN 1-58949-023-1, US$88
Results of the CADE Trustee Elections 2003
Herbrand Award: Call for Nominations
Call for Tutorial Proposals
Call for Papers
New Books
From the AAR President, Larry Wos...
Results of the CADE Trustee Elections 2003
Maria Paola Bonacina
(Secretary of AAR and CADE)
E-mail: mariapaola.bonacina@univr.it
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
F. Baader
48
26
17
25
116
P. Baumgartner
32
42
21
21
116
M. Kohlhase
28
24
25
39
116
S. Schulz
8
23
39
46
116
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
F. Baader
49
32
33
2
116
P. Baumgartner
35
49
29
3
116
M. Kohlhase
31
30
51
4
116
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
F. Baader
64
47
5
0
116
P. Baumgartner
50
60
6
0
116
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
P. Baumgartner
60
31
23
2
116
M. Kohlhase
39
32
42
3
116
S. Schulz
17
44
53
2
116
Candidate
1st pref.
2nd pref.
3rd pref.
4th pref.
Total
M. Kohlhase
64
48
3
1
116
S. Schulz
47
62
7
0
116
David Basin (IJCAR 2004 Program co-chair)
Peter Baumgartner (Elected 10/2003)
Maria Paola Bonacina (Secretary)
Gilles Dowek (Elected 9/2001)
Harald Ganzinger (Past program chair, elected 10/1999 and 10/2002)
John Harrison (Elected 9/2001)
Michael Kohlhase (Elected 10/2000 and 10/2003)
Neil V. Murray (Treasurer)
Frank Pfenning (President, elected 10/1998 and 9/2001)
Andrei Voronkov (Vice-President, past program chair, elected 10/2002)
Toby Walsh (Elected 10/2002)
Herbrand Award: Call for Nominations
Maria Paola Bonacina
Secretary of AAR and CADE
On behalf of the CADE Inc. Board of Trustees
Woody Bledsoe (1994)
Alan Robinson (1996)
Wu Wen-Tsun (1997)
Gerard Huet (1998)
Robert S. Boyer and J Strother Moore (1999)
William W. McCune (2000)
Donald W. Loveland (2001)
Mark E. Stickel (2002)
Peter B. Andrews (2003)
President of CADE Inc.
fp@cs.cmu.edu
Call for Tutorial Proposals - IJCAR 2004
Call for Papers
Universiteit Utrecht
Department of Philosophy
Heidelberglaan 8
3584 CS Utrecht, Netherlands
Vincent.vanOostrom@phil.uu.nl
Université Paris 12-IUT
Département Informatique
Route Forestière Hurtault
F-77300 Fontainebleau, France
Tel: +33.(0)1.60.74.68.16 (office)
Fax: +33.(0)1.60.74.68.28
E-mail: cegielski@univ-paris12.fr
Centro de Informatica
Univ. Fed. Pernambuco
Av. Prof. Luis Freire, s/n,
50740-540 Recife, PE, Brazil
Tel: +55 81 3271 9430
Fax: +55 81 3271 9438
E-mail: ruy@cin.ufpe.br
New Books
For more information see the
Web.
by Larry Wos and Gail W. Pieper
For more information see the
Web.
Gail W. Pieper
Technical editor
December 2003