No. 47, April 2000


From the AAR President
News from CADE Inc.

  • CADE-17
  • CADE-17 Workshops
  • CADE-17 ATP System Competition

  • Nominations for Herbrand Award
    Bledsoe Student Travel Award
    International Joint Conference on Automated Reasoning: A Manifesto
    Test Problem and Perl Scripts for Finite Model Searching
    An International Master's Program in Computational Logic
    Calls for Participation and/or Contributions
  • ESSLLI-2000
  • WoLLIC'2000

  • New Book on Automated Reasoning

    Abstracts of Recent Ph.D. Theses in AR

    From the AAR President, Larry Wos...

    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 (

    CADE News


    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 with ``subscribe" in the header to subscribe to this mailing list. Everybody is invited to submit challenges.

    CADE-17 ATP System Competition

    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.

    Call for Nominations for the Herbrand Award

    Maria Paola Bonacina (Secretary of AAR and CADE)

    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.

    with copies to

    Woody Bledsoe Student Travel Award:
    Call for Nominations

    Maria Paola Bonacina
    (On behalf of the CADE Board of Trustees)

    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 ( and

    David McAllester, CADE-17 Program Chair (,

    with copies to

    Ulrich Furbach, CADE President ( and

    Neil V. Murray, CADE Treasurer (

    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.

    International Joint Conference on
    Automated Reasoning: A Manifesto

    Maria Paola Bonacina
    (On behalf of the IJCAR Steering Committee)

    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.

    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 and Perl Scripts for Finite Model Searching

    Jian Zhang

    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:

    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.

    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.

    International Master's Program in Computational Logic

    Maja von Wedelstedt, secretary
    Artificial Intelligence Institute
    Dresden University of Technology

    The Dresden University of Technology is offering a two-year study program, in English, leading to a master of science in computational logic (together with a German ``Diplom in Informatik"). The program is sponsored by the European Network of Excellence in Computational Logic (COMPULOG Net) and other German institutions.

    Past and present teachers include Oskar Bartenstein, Maria Paola Bonacina, Catalin Buiu, Anatoli Degtyarev, Enrico Franconi, Alessio Guglielmi, Steffen Hoelldobler, Dieter Hutter, Michael Kohlhase, Giorgio Levi, Jim Lipton, Faron Moller, Michael Posegga, Horst Reichel, Joerg Siekmann, Werner Stephan, Michael Thielscher, Heiko Vogler, Andrei Voronkov, and Christoph Weidenbach.

    Courses focus on logic and constraint programming, artificial intelligence, type theory, model theory, proof theory, equational reasoning, databases, natural language processing, and planning and formal methods.

    The tuition fees are waived. At the end of the program a research master thesis must be presented.

    Prerequisites are a good knowledge of the basics of logic, and familiarity with mathematical reasoning. Knowledge of foundations of artificial intelligence and logic programming are desirable. Fluency in English is indispensable; German is not necessary, but there are facilities for studying it if desired. A bachelor in computer science, or and equivalent degree, is required by the beginning of courses, in October 2000.

    Deadline for applications is July 15, 2000. To apply, send an e-mail with your curriculum vitae to mailto:CL@Pikas.Inf.TU-Dresden.DE. Further information is on the Web at

    Call for Participation and/or Contributions


    On August 14--18, 2000, a Workshop on Hybrid Logics will take place as part of the Twelfth European Summer School in Logic, Language and Information, in Birmingham, Great Britain.

    Hybrid logics are modal languages that use "terms as formulas." Although they date back to the late 1960s, hybrid logics have seen a resurgence of interest recently, with new results in expressivity, interpolation, complexity, and proof techniques. It has also become clear that hybrid logics offer a theoretical framework for uniting the work of a surprisingly diverse range of research traditions.

    In particular, this workshop is devoted to exploring ideas Arthur Prior introduced 30 years ago. It will be an ideal opportunity to see how his ideas have been developed in the intervening period.

    Authors are invited to submit an extended abstract of a research paper (up to 10 pages) in PostScript format to before June 1, 2000.

    Please note that all workshop contributors are required by the ESSLLI organizers to register for the Summer School.

    Papers accepted for the workshop will be made available from the Hybrid Logic Site. Following the workshop, participants will be invited to submit their contributions for publication in a special issue of the Journal of Logic and Computation.

    Please visit the Web site for further information.


    The 7th Workshop on Logic, Language, Information and Computation will be held on August 15--18, 2000, in Natal, Brazil. Contributions are invited in the form of papers (up to 10 pages) in all areas related to logic, language, information and computation, ranging from pure logical systems and logic and complexity theory, to logic engineering, to artificial intelligence and automated deduction,

    Papers should be sent in PostScript format by e-mail to by May 7, 2000. The abstracts of the papers will be published in a ``Conference Report" section of the Logic Journal of the IGPL. Papers presented at the meeting will be invited for submission (in full version) to the Logic Journal of the IGPL.

    For further information, contact the chair of the organizing committee: Ruy de Queiroz,, or see the Web page.

    New Book

    A new book The Collected Works of Larry Wos by Larry Wos with Gail Pieper, has been published by World Scientific. This monumental work (more than 1600 pages) comprises two volumes: Volume 1 - Exploring the Power of Automated Reasoning, and Volume 2 - Applying Automated Reasoning to Puzzles, Problems, and Open Questions.

    The book has the following special features:

    New Journal Announced

    Krzysztof R. Apt (
    President of the Association for Logic Programming

    A new journal entitled Theory and Practice of Logic Programming (TPLP) will appear in January 2001.

    The founding editor of the new journal is Professor Emeritus Jack Minker of the University of Maryland. The board of editors comprises the 50 former editors of the Journal of Logic Programming (JLP), who resigned after unsuccessful negotiations with the publisher about the price of library subscriptions. The Association for Logic Programming, acting in full cooperation with the former editorial board of the JLP, has withdrawn its support for the JLP and has adopted TPLP as the sole official journal of the ALP.

    TPLP will initially be published bimonthly in both print and electronic form. For the current list of accepted papers please see the TPLP home page.

    Abstracts of Recent Ph.D. Theses in AR

    We are initiating a new section in the AAR newsletter featuring abstracts of recent doctoral dissertations in automated deduction and theorem proving. We believe that the work of these newest members of the automated reasoning community will be of interest to our AAR members.

    Author: Andrea Formisano

    Title: Theory-based Resolution and Automated Set Reasonin

    Advisor: Eugenio G. Omodeo

    Date of defense: March 24, 2000

    Institution granting the degree: Università La Sapienza di Roma

    Abstract: Recently, several authors introduced various theory-based extensions of basic inference procedures (the resolution procedure and the connection method, among others). A common philosophy inspired all of these new proposals: to endow the automated systems with some sort of "human skill," that is, give the system the capacity of exploiting semantical knowledge behind its ability of performing syntactical manipulations of formulas. In these systems the reasoning activity develops at two distinct levels: a foreground level, where an essentially syntactical framework is employed, and a background level, which is the repository of the semantic knowledge. In the case of T-resolution -- just one among the various proposals -- this knowledge takes the form of a decision procedure for the satisfiability of formulas of a underlying theory T that is a parameter of the whole system.

    In this context, two main streams of research deserve deep investigation. First, the properties of the T-resolution rule itself should be assessed. As an original contribution we present a technique à la Henkin for proving completeness of (generic) resolution-based calculi that avoids compactness assumptions. Then, the characteristics of the T-resolution procedure are analyzed in depth by considering its completeness, its mechanizability, and a number of its refinements. Second, we are interested in obtaining decidability results for specific theories. As a starting point, we present a repository of decision methods for fragments of set theory. In particular, we devise an algorithm for deciding -sentences on sets with self-singleton atoms (following a proposal of Quine).

    As a matter of fact, set theory is expressive enough to offer a firm ground for formalizing almost every mathematical concept. This argument motivates the efforts directed at characterizing its decidable fragments and at automating set-reasoning. As a contribution in this direction we give a reformulation of a number of first-order theories within a homogeneous framework such as the Tarski-Chin-Givant map calculus. As a consequence, the automation of the map calculus would offer an alternative approach to theory-reasoning. In order to reach this goal, we start by tackling the problem of translatability between first-order logic and map calculus; for instance, we show how the variety of (antithetic) possibilities offered by axiomatic set Theory can be forged within the map formalism. Then, we introduce the basics of map reasoning technology in order to set the ground for (a) the realization of a "stand-alone" platform for map reasoning, and (b) the implementation of a map reasoner on top of an existing first-order theorem prover. Finally, we report on an initial experimentation activity that yields automated proofs of fundamental properties of our axiomatizations; we face the problem of singling out a series of tactics for automated detection of legal set-abstraction; and we outline an innovative and promising approach to the decision problem for syllogistics.

    Author's correspondence address:
    Andrea Formisano
    Dipartimento di Matematica e Informatica,
    Università degli Studi di Perugia.
    Via Vanvitelli 1 - 06100 Perugia, Italy.
    E-mail: or