New CADE and AAR Secretary
Ganzinger to Receive Herbrand Award
Woody Bledsoe Student Travel Award
Call for Nominations: CADE Trustees Elections
IJCAR Tutorials
Call for Participation - IJCAR 2004
Announcement of CADE-20
Courses and Workshops Book and Software Announcement
The TSTP Solution Library
Ah, summer: It's a great time to relax. But for those
of you who are truly dedicated,
we present here announcements for
various summer schools, workshops, and conferences.
Dwarfing any summer occurrence is the good fortune that has
befallen both AAR and CADE.
In particular, Amy Felty has graciously agreed to be our new secretary.
She replaces Maria Paola Bonacina, who has done a marvelous job
as AAR secretary since 1997.
In the parlance of poker, all of us are indeed lucky to have
had Maria Paola's assistance and
to now have that of Amy.
One conference of particular note for AAR members is, of course, IJCAR.
In conjunction with this conference, I mention that Harald Ganzinger
will receive the 2004 Herbrand Award.
My congratulations to Harald!
We are pleased to announce that Amy Felty has agreed to serve as
secretary for AAR and CADE, starting with the present issue of the AAR
Newsletter. She will be taking over the duties of Maria Paola Bonacina
who resigned after many years of excellent and dedicated service. She
held the positions of secretary of AAR for seven years and secretary of
CADE for five years. Both AAR and CADE are deeply indebted to Maria
Paola, and we would also like to express our personal gratitude.
As CADE secretary, Amy Felty will be an ex-officio trustee. According
to the by-laws, her initial term is three years, although she can serve
any number of consecutive terms.
It is my distinct honor to announce on behalf of the Board of Trustees
of CADE Inc. that Harald Ganzinger
is to receive
the 2004 Herbrand Award for Distinguished Contributions to Automated Reasoning.
The award is to be given
in recognition of his seminal work on the theory underlying modern
theorem proving systems; the breadth of his research covering nearly all
major areas of deduction, and the depth of his results in each one of
them; his effective contributions to the development of systems and
implementation techniques; and his dedicated promotion of automated
reasoning both inside and outside the community.
The Woody Bledsoe Student Travel Award was created to honor
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 enable selected students to attend
the International Conference on Automated Deduction (CADE)
or the International Joint Conference on Automated Reasoning (IJCAR),
whichever is scheduled for the year, by covering much of their expenses.
In 2004, IJCAR will take place July 4-7,
in Cork, County Cork, Ireland.
For further information see
the
Web page.
The winners will be reimbursed (to a maximum of USD 600)
for their conference registration, transportation, and accomodation expenses.
Preference will be given to students who will play an active role in the
conference, including satellite workshops, and do not have alternative funding.
However, also students in other situations are encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words from
the student's supervisor.
Nominations for IJCAR 2004 should be sent by e-mail to
with copies to
Nominations must arrive no later than May 12, 2004,
and the winners will be notified by May 18, 2004.
The awards will be presented at IJCAR; in case a winner does not attend,
the chairs and trustees may transfer the award to another nominee
or give no award.
Nominations for three CADE trustee positions are being sought, in
preparation for the elections to be held this coming fall.
The board of trustees currently includes (in alphabetical order):
The term of Gilles Dowek, John Harrison, and Frank Pfenning expire after
IJCAR 2004, because CADE trustees are elected for three years. The term
of office of David Basin as program co-chair of IJCAR 2004 also ends.
Furthermore, Maria Paola Bonacina has resigned as CADE secretary.
Among the outgoing trustees, Gilles Dowek and John Harrison are eligible
to be nominated for a second term. David Basin and Maria Paola Bonacina
as outgoing ex-officio trustees are also eligible to be nominated for a
first term as elected trustees. Frank Pfenning is not eligible, having
served two consecutive terms.
Nominations can be made by any AAR member, either by e-mail or in person
at the IJCAR 2004 business meeting. Two members, a principal nominator
and a second, are required to make a nomination, and it is their
responsibility to ask people's permission before nominating them. A
member may nominate or second only one candidate. Nominees must be or be
willing to become AAR members. For further details please see the CADE
Inc. bylaws at the CADE
Web site.
E-mail nominations are to be sent to
cadeInc@site.uottawa.ca,
by the end
of IJCAR 2004 (July 8, 2004).
Dear Colleague:
It is my pleasure to announce that IJCAR 2004 is offering the
following five tutorials in the field of automated reasoning:
T4 - Automated Validation of Security Protocols (Jorge R. Cuellar, Sebastian Moedersheim, and Luca Vigano)
Detailed information about the tutorials is at
the
Web page.
Selected on a peer-review basis from a strong set of proposals, these
tutorials reveal the great diversity and vitality of automated
reasoning today.
The Second International Joint Conference on Automated Reasoning (IJCAR)
is the fusion of several major conferences in Automated Reasoning:
Registration to IJCAR 2004 is open: The deadline for early registration is
May 21, 2004.
Session topics are the following:
rewriting, saturation-based theorem proving,
interactive theorem proving, combination techniques,
verification and systems,
reasoning with finite structures,
tableaux and nonclassical logics, computer mathematics, higher-order
reasoning, combinatorial reasoning, and applications and systems.
Please see
the
Web page for all registration, accommodation,
and travel details, as well as the full technical program.
CADE-20 (2005) will be held in Tallinn, Estonia, which just joined the
European Union on May 1. Conference chair will be Tanel Tammet, Tallinn
University of Technology. Program chair will be Robert Nieuwenhuis,
Technical University of Catalonia. Tentative dates are
July 22-July 27, 2005, including workshops and tutorials. More details
will be available in a future edition of the AAR Newsletter.
ICCL Summer School and PCC Workshop 2004
A two-week meeting
consisting of two integrated parts, a summer school
and a workshop, will be held at the
Technische Universitaet Dresden June 1-26, 2004.
The themes
for the summer school are proof theory and automated theorem proving;
the
workshop is about proof, computation, and complexity.
The workshop is
aimed at graduate students and researchers.
from distinct but communicating
communities gathering in an informal and friendly atmosphere.
We ask for a participation fee of 200 EUR.
Please send an e-mail to
PTEvent@Janeway.Inf.TU-Dresden.DE, making sure you include a
brief bio (5-10 lines) stating your experience, interests, home page
(if available), and so forth. It will be possible for some students to present
their work: please indicate in your application if you would like to do
A limited number
of grants covering all expenses are available. Please indicate in your
application if the only possibility for you to participate is with a
grant. Applications for grants must include an estimate of travel costs,
and they should be sent together with the registration. We will provide
assistance in finding an accommodation in Dresden.
Week 1, June 14-18: courses on
June 21-22: workshop; for more details, please consult the workshop
Web page.
June 23-26: courses on
Logic Considered as a Branch of Geometry (Francois Lamarche, Loria & INRIA, Nancy)
ESSLLI-2005
The Seventeenth European Summer School in Logic, Language and Information
will be held at Heriot-Watt, Edinburgh, United Kingdom.
August 8-19, 2005.
The program committee invites proposals for foundational,
introductory, and advanced courses and for workshops for the 17th
annual summer school on a wide range of timely topics
relevant to
language and computation, language and logic, and logic and computation.
Proposals should be submitted by July 15, 2004, through a Web form
available at
the
Web page.
Courses
Courses are taught by 1 or 2 lecturers and
typically consist of five sessions (a one-week course) or ten sessions
(a two-week course). Each session lasts 90 minutes. Courses are given
on three levels.
Foundational Courses: These are elementary courses not assuming
any background knowledge. They are intended for people to get
acquainted with the problems and techniques of areas new to them.
Ideally, they should allow researchers from other fields to acquire
the key competences of neighboring disciplines, thus encouraging the
development of a truly interdisciplinary research community.
Foundational courses may presuppose some experience with scientific
methods in general, so as to be able to concentrate on the issues that
are germane to the area of the course.
Introductory Courses: Introductory courses are central to the
activities of the Summer School. They are intended to equip students
and young researchers with a good understanding of a field's basic
methods and techniques. Introductory courses in
can build on some knowledge of the component
fields;
for example, an introductory course in computational linguistics
should address an audience familiar with the basics of
linguistics and computation. Proposals for introductory courses
should indicate the level of the course as compared to standard texts
in the area (if available).
Advanced Courses: Advanced courses should be pitched at an audience of
advanced master's or doctoral students. Proposals for advanced courses
should specify the prerequisites in some detail.
Workshops
The aim of the workshops is to provide a forum for advanced
Ph.D. students and other researchers to present and discuss their
work. Each workshop centers on a specific theme;
the
organizers should be specialists in the theme of the workshop and give
a general introduction in the first session. A workshop consists of
five sessions (one week). Sessions are normally 90 minutes.
To obtain further information, visit the ESSLLI
site through
the
Web page. For this year's summer school,
please see the
Web site
for ESSLLI-2004.
Design of Logic-based Intelligent Systems, by
Klaus Truemper
The book covers a framework of ideas and algorithms that, in a
unified treatment, support construction of intelligent
systems for far-ranging tasks such as medical diagnosis,
music composition, management of hazardous processes and
materials, traffic control, evaluation of credit worthiness,
natural language processing. The approach is based on an
extension of propositional logic.
Contents
The publication of the book is accompanied by release of
version 6.0 of the Leibniz Systems software, which
has most algorithms of the book implemented. The software allows
For further details, see the
Web site.
In November 1993 Christian Suttner and I released the first version of the TPTP
Problem Library, 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. Since its first release, many
researchers have used the TPTP as an appropriate and convenient basis for ATP
system evaluation. Now I've started nailing my other foot to the floor.
The TSTP (Thousands of Solutions from Theorem Provers) Solution Library is a
library of solutions to test problems for ATP systems. The TSTP supplies the
ATP community with
An early version TSTP is now available online at
the
Web site.
This early version contains the output from 33 ATP systems on all the TPTP
problems. The solutions are updated regularly as new problems, systems, and
system versions become available.
Each TSTP file contains the following:
In the future the TSTP will be extended to include
The ATP community is invited to look at the TSTP, use it, and provide feedback
for improvement.
Reference
[SZS03] Sutcliffe, G., Zimmer, J., and Schulz, S.,
``Communication Standards for Automated Theorem Proving Tools,''
pp. 52-57
in
Proceedings of the Workshop on Agents and Automated Reasoning, 18th
International Joint Conference on Artificial Intelligence,
Acapulco, Mexico,
edited by V. Sorge, S. Colton, M. Fisher, and J. Gow,
2003.
From the AAR President, Larry Wos...
New CADE and AAR Secretary
Larry Wos, President of AAR, and Frank Pfenning, President of CADE, Inc.
Ganzinger to Receive Herbrand Award
Frank Pfenning
President of CADE Inc.
Woody Bledsoe Student Travel Award:
Maria Paola Bonacina
Call for Nominations
(On behalf of the CADE Inc. Board of Trustees)
(basin@inf.ethz.ch and Michael.Rusinowitch@loria.fr)
and
Toby Walsh and Barry O'Sullivan, IJCAR 2004 Conference Chair and Vice-Chair
(tw@4c.ucc.ie and b.osullivan@cs.ucc.ie)
and
Neil V. Murray, CADE Inc. Treasurer (nvm@cs.albany.edu).
Call for Nominations: CADE Trustees Elections
Amy Felty, AAR and CADE Secretary
IJCAR Tutorials
William Farmer
IJCAR 2004 Tutorials Chair
wmfarmer@mcmaster.ca
Call for Participation - IJCR 2004
These five events will join for the first time at the IJCAR conference
in Cork in July 2004.
Preliminary Announcement of CADE-20
Frank Pfenning, President of CADE, Inc.
Courses and Workshops
Week 2
For further information, see the
Web site.
Paris 7)
Book and Software Announcement
May 2004
2. Basic Formulation and Reasoning Techniques
3. Learning Logic Formulas from Data
4. Nonmonotonicity, Incompleteness, Futility
5. Question-and-Answer Processes
6. Examples of Intelligent Systems
The book includes instructions for free-of-charge downloading
and use of the software. The software is supplied in source
code form and may be used without restriction in commercial
and noncommercial projects.
The TSTP Solution Library
Geoff Sutcliffe
Department of Computer Science, University of Miami
geoff@cs.miami.edu; http://www.cs.miami.edu/
geoff
Gail W. Pieper
Technical editor
May 2004