AARNEWS - April 2002



No. 55, April 2002


From the AAR President
Herbrand Award: Call for Nominations
Proposals for Sites for IJCAR 2004 Solicited
Call for Papers

  • CADE-18 Workshop: Problems and Problem Sets for ATP
  • Complexity in Automated Deduction
  • Mathematical Knowledge Management
  • Thesis Abstracts
    CologNet: New European Network of Excellence on Computation and Logic
    Summer School on Computational Logic

    From the AAR President, Larry Wos...

    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.

    Herbrand Award:
    Call for Nominations

    Maria Paola Bonacina
    Secretary of AAR and CADE
    On behalf of the CADE Inc. Board of Trustees

    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)
    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).

    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

    Ulrich Furbach
    President of CADE Inc.
    with copies to bonacina@cs.uiowa.edu.

    Proposals for Sites for IJCAR 2004 Solicited

    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:

    1. National, regional, and local AR community support:
    2. National, regional, and local government and industry support, both organizational and financial.
    3. Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
    4. Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls).
    5. Conference and exhibit facilities for the anticipated number of registrants (minimum 250 - the size of IJCAR 2001), for example,
    6. Residence accommodations and food services in a range of price categories and close to the conference facilities, for example,
    7. Rough budget projections for the various budget categories, e.g.,
    8. Balance with regard to the geographical distribution of previous IJCAR and its constituent meetings.

    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.


    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

    Alessandro Armando (armando@dist.unige.it) (FroCoS Representative)
    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)

    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).

    Call for Papers

    CADE-18 Workshop: Problems and Problem Sets for ATP

    Geoff Sutcliffe, Jeff Pelletier, Christian Suttner
    Workshop Organizers

    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.

    2nd International Workshop on Complexity in Automated Deduction

    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:

    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.

    MKM 2003

    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:

    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.

    Thesis Abstracts

    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.

    New European Network of Excellence on Computation and Logic

    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.

    Summer School on Computational Logic

    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
    April 2002