AARNEWS - May 2004



No. 63, May 2004

From the AAR President
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

  • ICCL Summer School/ PCC Workshopo
  • ESSLLI-2005
  • Book and Software Announcement
    The TSTP Solution Library

    From the AAR President, Larry Wos...

    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!

    New CADE and AAR Secretary

    Larry Wos, President of AAR, and Frank Pfenning, President of CADE, Inc.

    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.

    Ganzinger to Receive Herbrand Award

    Frank Pfenning
    President of CADE Inc.

    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.

    Woody Bledsoe Student Travel Award:
    Call for Nominations

    Maria Paola Bonacina
    (On behalf of the CADE Inc. 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) 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

    David Basin and Michael Rusinowitch, IJCAR 2004 Program Co-Chairs
    (basin@inf.ethz.ch and Michael.Rusinowitch@loria.fr)
    Toby Walsh and Barry O'Sullivan, IJCAR 2004 Conference Chair and Vice-Chair
    (tw@4c.ucc.ie and b.osullivan@cs.ucc.ie)

    with copies to

    Frank Pfenning, CADE Inc. President (fp@cs.cmu.edu)
    Neil V. Murray, CADE Inc. Treasurer (nvm@cs.albany.edu).

    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.

    Call for Nominations: CADE Trustees Elections

    Amy Felty, AAR and CADE Secretary

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

  • Franz Baader (CADE-19 Program Chair, elected 10/2003)
  • David Basin (IJCAR 2004 co-Program Chair)
  • Peter Baumgartner (elected 10/2003)
  • Maria Paola Bonacina (Secretary, appointed 9/1999, resigned 5/2004)
  • Gilles Dowek (Elected 9/2001)
  • Amy Felty (Secretary, appointed 5/2004)
  • Harald Ganzinger (CADE-16 Program Chair, elected 10/1999, reelected 10/2002)
  • John Harrison (Elected 9/2001)
  • Michael Kohlhase (Elected 10/2000, reelected 10/2003)
  • Neil Murray (Treasurer)
  • Robert Nieuwenhuis (Program Chair, CADE-20)
  • Frank Pfenning (President, elected 10/1998, reelected 9/2001)
  • Andrei Voronkov (Vice President, CADE-18 Program Chair, elected 10/2002)
  • Toby Walsh (elected 10/2002)
  • 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).

    IJCAR Tutorials

    William Farmer
    IJCAR 2004 Tutorials Chair

    Dear Colleague:

    It is my pleasure to announce that IJCAR 2004 is offering the following five tutorials in the field of automated reasoning:

    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.

    Call for Participation - IJCR 2004

    The Second International Joint Conference on Automated Reasoning (IJCAR) is the fusion of several major conferences in Automated Reasoning:

    These five events will join for the first time at the IJCAR conference in Cork in July 2004.

    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.

    Preliminary Announcement of CADE-20

    Frank Pfenning, President of CADE, Inc.

    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.

    Courses and Workshops

    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

    Week 2

    June 21-22: workshop; for more details, please consult the workshop Web page.

    June 23-26: courses on

    For further information, see the Web site.


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


    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.

    Book and Software Announcement

    Design of Logic-based Intelligent Systems, by Klaus Truemper

    Publisher: John Wiley & Sons
    May 2004

    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.


    1. Introduction to Intelligent Systems
    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 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

    1. Logic computation to be embedded into C or C++ code, via the compiler lbcc of the Leibniz System
    2. Learning of logic formulas from data, including transformation of rational data and set data to logic data, using the programs lsqcc and cutcc

    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.

    For further details, see the Web site.

    The TSTP Solution Library

    Geoff Sutcliffe
    Department of Computer Science, University of Miami
    geoff@cs.miami.edu; http://www.cs.miami.edu/$\sim$geoff

    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.


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

    Gail W. Pieper
    Technical editor
    May 2004