NEWSLETTER
No. 47, April 2000
Contents
From the AAR President
News from CADE Inc.
The CADE-17 conference will soon be upon us, and, in addition to the
presentations, several exciting workshops are planned.
Here we briefly describe three of these.
Also presented is the call for nominations for the Herbrand Award
that was sent to the membership by e-mail in mid-February 2000.
This award traditionally is presented at the CADE conference in recognition of
exceptional contributions to the field.
The newsletter also has
details about the Woody Bledsoe Travel Award, which will help pay expenses for students wishing to attend CADE.
Most significant is the Manifesto
in which is proposed an international joint conference on automated
reasoning instead of the several diverse conferences that have threatened
to weaken our community. I urge you to carefully consider the issues presented
and to send in your comments and suggestions.
I am pleased to see included in this issue the
abstract of a newly completed dissertation in the field of automated reasoning.
I hope we will see more such contributions, as well as follow-on
articles from these new members of the AAR community.
Please encourage your students to send items to
our editor,
Gail Pieper (pieper@mcs.anl.gov).
CADE-17
The 17th International Conference on Automated Deduction
will take place on June 17--20, 2000, at
Carnegie Mellon University in Pittsburgh, Pennsylvania.
Continuing the tradition of recent CADEs, there are 6 affiliated workshops
and 4 tutorials on the days preceding and following the main conference
program, June 16 and June 21. The system competition (CASC-17) will
be held on June 17. Calls for contributions to several workshops and CASC
system registration are still open!
For further information, see the
Web site.
CADE-17 Workshops
In our last AAR newsletter, we included announcements about two workshops
that will be held in conjunction CADE-17
in Pittsburgh.
Below are the announcements of two additional workshops planned for that
meeting.
1. The Role of Automated Deduction in Mathematics
The purpose of this workshop is to discuss the role of automated
deduction in all areas of mathematics. This will include looking at
the interaction between automated deduction programs and other
computational systems that have been developed over recent years to
automate different areas of mathematical activity. Such systems
include computer algebra packages, tutoring programs, systems
developed to help explore a mathematical theory, and those developed
to help present and archive mathematical theories.
In all these fields automated deduction is either already used or
could be fruitfully employed to enhance the power and reliability of
existing systems.
We hope to attract papers discussing the theoretical frameworks for
such integration as well as papers detailing particular
implementations. Demonstrations of systems combining deduction systems
with other mathematical software are encouraged.
We also hope to attract papers discussing the use of automated
deduction for mathematical research.
See the
workshop
home page for more information.
2. Automation of Proofs by Mathematical Induction
Proof by mathematical dnduction presents the automated deduction
community with some very challenging research problems. The aim of
this one-day workshop is to create an informal forum in which
hot topics and emerging techniques can be presented and discussed.
The workshop will feature invited talks and contributed presentations,
with ample time for discussion of areas including
inductive theorem proving and formal methods,
higher-order inductive theorem proving,
integrating inductive and high-performance theorem provers,
and solutions to challenging problems.
Consistent with the workshop format, we expect and encourage
contributed talks to present work in progress, rather than polished
final results. In addition, we encourage system users to report on
their solutions to ``challenges"---informal
problem descriptions that we distribute through a moderated mailing
list and the workshop
Web page.
Send mail to challenge-request@twelf.org
with ``subscribe" in the header to subscribe to this mailing list.
Everybody is invited to submit challenges.
The CADE conferences are the major forum for the presentation of new research
in all aspects of automated deduction. In order to stimulate ATP system
development and to expose ATP systems to interested researchers, an ATP system
competition (CASC-17) will be held at CADE-17 on Saturday, June 17, 2000.
CASC-17 will evaluate the performance of sound, fully automatic, 1st order ATP
systems. The evaluation will be in terms of
the number of problems solved and
the average runtime for successful solutions,
in the context of
(1) a bounded number of eligible problems, chosen from the
TPTP Problem Library, and
(2) a specified time limit for each solution attempt,
The competition organizers are Geoff Sutcliffe and Christian Suttner. The
competition will be overseen by a panel of knowledgeable researchers who are
not participating in the event.
Further details and registration information are available at
the
Web page.
System registration for CASC-17 closes on May 15, 2000.
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 meeting.
Whether and to whom an award will be given is decided by the CADE
Trustees, the current CADE Program Committee, and previous
recipients of the award.
The Herbrand Award has been given in the past to Larry Wos (1992)
Woody Bledsoe (1994), Alan Robinson (1996), Wu Wen-Tsun (1997),
Gerard Huet (1998), and Robert S. Boyer and J Strother Moore (1999).
A nomination is required for consideration for the Herbrand award.
Nominations can be made at any time and remain open indefinitely,
but only nominations received by 15 March 2000 will be considered for a
Herbrand Award at CADE-17 in June 2000.
Nominations should consist of a letter (preferably e-mail) 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
Ulrich Furbach, President of CADE Inc.
uli@informatik.uni-koblenz.de
with copies to bonacina@cs.uiowa.edu.
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)
by covering much of their expenses. CADE-17 will take place from
June 17 to 20, 2000 in Pittsburgh, Pennsylvania, USA (for further information
see the
Web page).
The winners will be reimbursed (to a maximum of USD$600)
for their conference registration, transportation, and accommodation expenses.
Preference will be given to students who do not have alternative funding.
While preference will be given to students who will play an active role in the
conference, including the attached workshops, also students who do not
expect to give presentations, including students who have just begun their
research in automated deduction or are considering the field,
are encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words from
the student's supervisor. Nominations for CADE-17 should be sent by e-mail to
Frank Pfenning, CADE-17 Conference Chair (fp@cs.cum.edu) and
David McAllester, CADE-17 Program Chair (dmac@research.att.com),
with copies to
Ulrich Furbach, CADE President (uli@informatik.uni-koblenz.de) and
Neil V. Murray, CADE Treasurer (nvm@cs.albany.edu).
Nominations must arrive no later than April 20, 2000,
and the winners will be notified by May 1, 2000.
The awards will be presented at CADE-17; in case a winner does not attend,
the trustees may transfer the award to another nominee or give no award.
The past ten years have seen a gradual fragmentation of the automated
reasoning community into various disparate groups, each with its own
conference. During 1999 various members of the CADE, FTP,
and TABLEAUX communities have discussed the idea of holding a joint
conference in 2001 to try to bring our groups together.
This debate has produced a project to hold an
International Joint Conference on Automated Reasoning (IJCAR)
in Siena (Italy) from Monday, June 18, to Saturday, June 23, 2001.
This is a one-time proposal for 2001; after the first IJCAR the three
communities may discuss whether and how to continue.
The following points have emerged after various discussions inside
each group and among the groups.
Maria Paola Bonacina, University of Iowa (FTP)
This document was composed by the IJCAR Steering Committee in the
early months of 2000, after the CADE Board of Trustees, the FTP Steering
Committee, and the TABLEAUX 2000 Program Committee agreed to have IJCAR
in the course of the summer and fall of 1999.
Comments and suggestions from all members of the AAR community
are very welcome and will be carefully listened to.
The IJCAR Steering Committee thanks the CADE Board of Trustees,
the FTP Steering Committee and the TABLEAUX 2000 Program Committee,
for their support, and all the people mentioned in this document
for their efforts so far and their willingness to serve the
Automated Reasoning community through the IJCAR initiative.
Test Problem.
Let us consider the linear-time temporal logic (LTL), whose formulas
have finite models. To describe LTL structures using first-order logic,
we use the predicate symbol R and the function symbol s,
which denote "less-than-or-equal-to" and "successor", respectively.
It can be proved that the following axioms characterize LTL structures
of size n:
Perl scripts for SEM users.
The finite model searching program
SEM accepts many-sorted
first-order clauses as input. To use it, one also has to specify the sizes
of the domains. Sometimes it is more convenient to write first-order formulas
with quantifiers. Here are several Perl scripts
to facilitate the use of SEM. They make use of the theorem prover
OTTER, which should be
installed first. Given a set of (uni-sorted) first-order formulas, a set of clauses
are generated, and SEM is asked to search for models of increasingly larger sizes.
From the AAR President, Larry Wos...
CADE News
CADE-17 ATP System Competition
Call for Nominations for the Herbrand Award
Maria Paola Bonacina
(Secretary of AAR and CADE)
Woody Bledsoe Student Travel Award:
Maria Paola Bonacina
Call for Nominations
(On behalf of the CADE Board of Trustees)
International Joint Conference on
Maria Paola Bonacina
Automated Reasoning: A Manifesto
(On behalf of the IJCAR Steering Committee)
For TABLEAUX, the co-chair is Rajeev Gore (Australian National University),
selected by the Program Committee of TABLEAUX 2000.
For FTP, the co-chair is Alexander Leitsch (Technische Universität Wien),
selected by the Steering Committee of FTP.
For CADE, the co-chair is Tobias Nipkow (Technische Universität München),
selected by the CADE Board of Trustees.
It is expected that the three Program Co-Chairs will choose a balanced
program committee with significant representation from all participating
communities.
IJCAR will invite submission related to all aspects of automated
reasoning, including foundations, implementations, and applications.
The Workshop Chair will be responsible for the selection of the workshops in
cooperation with the Program Co-Chairs and Conference Chair, according to
the indications of the Program Committee. He will be in charge of keeping all
the correspondence with perspective and actual workshop organizers, and will be
the interface between the workshop organisers and the conference organization.
The Tutorial Chair will be responsible for the selection of the tutorials in
cooperation with the Program Co-Chairs and Conference Chair, according to
the indications of the Program Committee. He will be in charge of keeping all
the correspondence with perspective and actual speakers, and will be
the interface between the tutorial speakers and the conference organization.
The Treasurer and the Conference Chair will handle finances, and,
in consultation with the Steering Committee, will find a
fair procedure for the parent events to share financial risks and profits.
For 2001 this rule produces the following Steering Committee
(in alphabetical order):
Ricardo Caferra, LEIBNIZ-IMAG Grenoble (FTP)
Ulrich Furbach, Universität Koblenz-Landau (CADE)
Rajeev Gore, Australian National University (TABLEAUX)
Alexander Leitsch, Technische Universität Wien (FTP)
Fabio Massacci, Università di Siena (TABLEAUX)
Tobias Nipkow, Technische Universität München (CADE)
Frank Pfenning, Carnegie Mellon University (CADE)
Peter Schmitt, Universität Karlsruhe (TABLEAUX)
Test Problem and Perl Scripts for Finite Model Searching
Jian Zhang
(zj@ox.ios.ac.cn,
Jian.Zhang@imag.fr)
For example, to generate LTL structures of size 4, we may give the following input
to SEM:
( elem [4] )
{ R: elem elem -> BOOL }
{ s: elem -> elem }
[ R(x,x) ]
[ -R(x,y) | -R(y,z) | R(x,z) ]
[ R(x,y) | R(y,x) ]
[ s(x) != y | R(x,y) ]
[ -R(x,y) | y = x | y = s(x) | y = s(s(x)) | y = s(s(s(x))) ]
And we get 23 models in total. But each of them is isomorphic to one of 4 models.
In fact, for a positive integer n, there are n distinct LTL structures.
The challenge is to eliminate as much isomorphism as possible.