NEWSLETTER
No. 55, April 2002
Contents
From the AAR President
Herbrand Award: Call for Nominations
Proposals for Sites for IJCAR 2004 Solicited
Call for Papers
Our spring issue brings several announcements about what to do with your summer.
Perhaps you wish to attend summer school in Italy;
the Second International Summer School on Computational Logic will take place in late August in Maratea.
Or perhaps you wish to sponsor a summer workshop;
the new CologNet welcomes ideas.
Or--and this I dearly hope--you wish to attack new problems in automated theorem proving; then you should contact Geoff Sutcliffe with ideas for
the CADE-18 workshop being planned.
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.
Nominations can be made at any time and remain open indefinitely,
but only nominations received by
April 1, 2002,
will be considered for a Herbrand Award at CADE in July 2002.
Note: An announcement about the Herbrand Award
nomination deadline was sent to all AAR members at the end of January.
Nominations should consist of a letter (preferably email) of up to
2,000 words from the principal nominator, describing the nominee's
contribution, along with letters of up to 2,000 words of endorsement
from two other seconders. Nominations should be sent to
We invite proposals for sites around the world to host the Second
International Joint Conference on Automated Reasoning (IJCAR) to be
held in summer 2004. The first IJCAR was held in Siena, Italy, in late
June 2001, merging CADE (Conference on Automated Deduction), FTP
(Workshop on First-order Theorem Proving) and TABLEAUX (Conference on
Analytic Tableaux and Related Methods), see
the
Web site.
The second IJCAR will be a merger of CADE, FTP, TABLEAUX, FroCoS
(Workshop on Frontiers of Combining Systems) and possibly other
events. Satellite workshops, tutorials and co-located events are
expected. Draft proposals are normally due about two years prior to
the expected conference date, hence by June 15, 2002,
for IJCAR 2004. In addition, we encourage proposers to register their
intention informally as soon as possible. Points of contact are given
below.
The final selection of the site will be made within two months after the
proposal due date.
Proposals should address the following points that also represent
criteria for evaluation:
cost of renting/cleaning the meeting rooms, if applicable,
Perspective organizers are encouraged to get in touch with one or more
contact people (see list below) for informal discussion.
If the host institution is not actually located at the proposed site,
then one or more visits to the site by the proposers is encouraged.
Contacts:
Please submit your proposal (plain ASCII preferred, otherwise PDF),
as well as any questions, to ijcar-tmp@informatik.uni-koblenz.de.
This is a temporary mailing list that will be replaced by one
at the site of IJCAR 2004 once decided. Currently, it includes
Supporting committees:
CADE Trustees: CADE-trustees@cs.uiowa.edu
Maria Paola Bonacina (Secretary), Gilles Dowek, Ulrich Furbach (President),
Harald Ganzinger, John R. Harrison, Michael Kohlhase, David McAllester,
Neil V. Murray (Treasurer), Frank Pfenning (Vice-President),
David A. Plaisted, Andrei Voronkov.
FroCoS Steering Committee: frocos-sc@mrg.dist.unige.it
Alessandro Armando, Franz Baader, Christoph Ringeissen, Klaus U. Schulz.
FTP Steering Committee: ftp-sc@logic.at
Alessandro Armando, Peter Baumgartner, Maria Paola Bonacina (President),
Ricardo Caferra, Domenico Cantone, David Crocker, Ingo Dahn, Bernhard Gramlich,
Reiner Haehnle, Alexander Leitsch, Paliath Narendran, Christoph Weidenbach.
TABLEAUX Steering Committee: reiner@cs.chalmers.se
Marcello D'Agostino, Uwe Egly, Chris Fermueller, Melvin Fitting, Ulrich Furbach,
Didier Galmiche, Rajeev Gore, Reiner Haehnle (President), Fabio Massacci,
Peter H. Schmitt (Vice-President).
In recent years there has been impressive progress in the development of
high-performance ATP systems, and ATP systems are becoming more and more
useful as tools of research and commercial application. As the use of ATP
systems expands to harder problems and new domains, it is important place
new problems and problem types in public view, to foster the development
of ATP systems and techniques that will better serve users' needs.
In order to expose and collect new ATP problems, we are running a workshop
at CADE-18 that will bring together real ATP system users and developers
in an environment focused on problems and problem sets for ATP systems.
Invited speakers at the workshop will be
John Harrison (Intel Corporation) and
Johannes Schumann (Automated Software Engineering Group, NASA Ames).
Details of the workshop are available at
the
Web site.
Submission of papers for presentation at the workshop is now invited.
We are particularly interested in submissions from commercial ATP users.
Submissions must be in PDF or Postscript, with a print area of 16cm x 23cm
(6.5in x 9in). There is no page limit, but extremely long listings of
problems or computer output should be relegated to a referenced WWW site.
All problems and problem sets must be available on the WWW, and the WWW
site referenced in the paper.
Submissions must be emailed to Geoff Sutcliffe
(geoff@cs.miami.edu), by Friday, April 19, 2002.
The Workshop on Complexity in Automated Deduction.
a satellite workshop of CADE-18
(in the conference FLoC'02),
will take place in Copenhagen, Denmark, July 25-26, 2002.
New deadline: May 10, 2002
The Workshop on Complexity in Automated Deduction will bring
together researchers who work on or have a serious interest in
problems that are in the interface between automated deduction
and computational complexity. The aim of the workshop is to
enhance the interaction between automated deduction and
computational complexity through invited and contributed talks
that will present comprehensive overviews, report on
state-of-the art advances, and expand the horizons of this area
of research.
Invited speakers:
From the AAR President, Larry Wos...
Herbrand Award:
Maria Paola Bonacina
Call for Nominations
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).
President of CADE Inc.
uli@informatik.uni-koblenz.de
Proposals for Sites for IJCAR 2004 Solicited
Maria Paola Bonacina (bonacina@cs.uiowa.edu) (FTP President)
Ulrich Furbach (uli@informatik.uni-koblenz.de) (CADE President)
Reiner Haehnle (reiner@cs.chalmers.se) (TABLEAUX President)
Fabio Massacci (massacci@ing.unitn.it) (IJCAR 2001 Conference Chair)
Call for Papers
CADE-18 Workshop: Problems and Problem Sets for ATP
Geoff Sutcliffe, Jeff Pelletier, Christian Suttner
Workshop Organizers
2nd International Workshop on Complexity in Automated Deduction
| Marco Cadoli | (Universite di Roma La Sapienza, Roma, Italy) |
| Hubert Comon | (LSV, ENS Cachan, France) |
| Erich Grüdel | (RWTH Aachen, Germany) |
| Martin Grohe | (University of Edinburgh, UK) |
| Phokion G. Kolaitis | (University of California, Santa Cruz, USA) |
| Paliath Narendran | (SUNY Albany, USA) |
| Reinhard Pichler | (Siemens AG Austria and TU Wien, Vienna) |
| Pavel Pudlak | (Mathematical Institute, Academy of Sciences, |
| Prague, Czech Republic) | |
| Andrei Voronkov | (University of Manchester, UK) |
In addition to the invited presentations, there will be contributed talks. If you are interested in giving such a contributed talk, please send an abstract, preferably as a PostScript attachment, to Miki.Hermann@loria.fr by Friday, May 10, 2002. Authors will by notified of acceptance on May 31, 2002. The final versions of accepted papers are due on June 7, 2002.
A selection of the best papers will take place after the workshop. The selected papers, which will undergo the usual refereeing process, will be published in a special issue of the journal Theory of Computing Systems (formerly Mathematical Systems Theory. To be eligible for this selection, the contributions must be original research papers. No surveys will be considered for selection.
For further information, please see the
Web site.
The Second International Conference on Mathematical Knowledge Management
will take place on February 16-18, 2003,
in Bertinoro, Italy (residential Centre of the University of Bologna).
Mathematical knowledge Management is an exciting new field in the
intersection of mathematics and computer science.
We need efficient, new techniques--based on sophisticated formal
mathematics and software technology--for taking fruit of the enormous
knowledge available in current mathematical sources and for organizing
mathematical knowledge in a new way. On the other side, because of its
very nature, the realm of mathematical information looks like the best
candidate for testing innovative theoretical and technological solutions
for content-based systems, interoperability, management of machine
understandable information, and the semantic Web.
The conference seeks to bring together math researchers, software
developers, publishing companies, math organizations, and teachers for
exchanging views and approaches and for pushing the field.
The conference organizers are seeking original contributions on theoretical,
technological and pragmatical aspects of mathematical knowledge
management. Papers focused on system/projects descriptions and comparison,
standardization efforts, critical surveys, large experimentations,
and case studies of mathematical knowledge management are particularly
welcome.
Topics of interest include the following:
MKM 2003
| Authoring languages and tools | MathML- and XML-based standards |
| Computer algebra systems | Metadata |
| Data mining | Theorem proving |
| Digital libraries | Proof assistants |
| Interactive learning | Searching and retrieving |
| Interoperability | Web publishing |
The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. The deadline for submissions is September 1, 2002. Papers (max. 12 pages) prepared according to the Authors Instructions of LNCS.
Authors will be required to send, besides the printed papers, the electronic source files of all parts of the manuscript (including front matter pages).
For further information, see the Web page.
Title: Model Building for Sets of Guarded Clauses
Author: Michael Dierkes
Advisor: Ricardo Caferra
Defense date: April 2001
Institution: Institut National Polytechnique de Grenoble, France
Abstract: During the past few years, automated model building has emerged as an important subfield of Automated Deduction. Its goal is to construct automatically (the description of) a model for a given satisfiable logical formula in such a way that the model can be used for useful computational operations as the evaluation of atoms and clauses.
In this thesis, we deal with the problem of building infinite and finite models for satisfiable sets of guarded clauses (without equality) automatically. Guarded clauses are clausal forms of formulas of the guarded fragment of first-order logic, which generalises minimal modal logics, inheriting from these logics nice properties as decidability and the finite model property. The guarded fragment and its derivations have turned out to be a very fruitful concept promising numerous applications. General finite model building systems can not take advantage of the special properties of the guarded fragment. It was therefore necessary to design special methods for guarded clauses.
The model building method for satisfiable sets of guarded clauses presented in this thesis is an extension of a resolution decision procedure. A given satisfiable set E of guarded clauses is first saturated under resolution, and then transformed into a set E' of guarded Horn clauses of a special form representing a Herbrand model for E. It is possible to evaluate guarded clauses in the model represented by E', but E' can also be used in order to find a finite model for E. We show that our method can easily be generalized to loosely guarded clauses, which are a generalisation of guarded clauses. We also present a model building method for weakly guarded Horn clauses. Weakly guarded clauses are another generalisation of guarded clauses.
The theoretical results of this thesis have been implemented in the GUAMO (GUArded clause set MOdel builder) system. GUAMO allows to build automatically a finite model for a given satisfiable set of guarded clauses. We present some experimental results obtained with GUAMO. For example, finite Kripke models for certain modal formulas can be built. A practical application might be the automated generation of finite state machines from specifications written in form of modal formulas.
The thesis (written in French) is available at the Web site.
The European Commission has recently decided to find a new network
that follows on from Compulog but has an even broader appeal. The
network will cover all aspects of logic in computation. Area chairs
will cover themes such as agents and logic, constraints and logic,
databases and logic, and automated reasoning. Toby Walsh (tw@cs.york.ac.uk)
is the area chair for automated reasoning. Like Compulog, CologNet
will support a number of activities, including summer schools,
and workshops. Please contact Toby Walsh for more details or if
you are running an event that you feel might attract support.
The Second International Summer School on Computational Logic
will be held August 25-30, 2002, in Maratea, Italy.
Computational logic (CL), the topic of the school, has many
applications, including the modeling of intelligent systems,
verification of software, and the support of systems for solving
computationally hard problems. Moreover, being founded on mathematical
logic, tools based on CL are themselves amenable to safe optimization
and verification techniques.
The school is aimed at graduate students as well as other researchers
interested in computational logic, both from university and from
industry. It will consist of several lectures covering both the
theoretical framework and relevant practical perspectives.
The deadline for reduced registration fee is May 15.
For further information, please see the
Web site.
prepared by Gail W. Pieper
CologNet:
New European Network of Excellence
on Computation and LogicSummer School on Computational Logic
April 2002