AARNEWS - May 2005



No. 67, May 2005

From the AAR President
Davis to Receive 2005 Herbrand Award
Woody Bledsoe Student Travel Award: Call for Nominations
Call for Nominations: CADE Trustees Election
CADE-20: Call for Participation
CADE ATP System Competition
Call for Papers

  • Trends in Logic III
  • LPAR-12
  • FLoC'06
  • Call for Abstracts of Theses

    From the AAR President, Larry Wos...

    My congratulations to Martin Davis as winner of this year's Herbrand Award! The progress in the field of automated reasoning in the past 40 years is amazing, and contributions such as Martin's deserve to be acknowledged.

    I encourage AAR members to participate in the CASC competition. This is one way to demonstrate how much our automated reasoning programs have advanced. Of course, I cannot resist the opportunity to also encourage you to attack open questions in various fields.

    Davis to Receive 2005 Herbrand Award

    Franz Baader
    President of CADE Inc.

    It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Martin Davis is to receive the 2005 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role as

    and his numerous other contribution to the field.

    Woody Bledsoe Student Travel Award:
    Call for Nominations

    Amy Felty (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 2005, CADE will take place July 22-27, in Tallinn, Estonia (for further information see the Web). The winners will be reimbursed (to a maximum of USD 800) for their conference registration, transportation, and accommodation 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 very much encouraged to apply.

    A nomination consists of a recommendation letter of up to 300 words from the student's supervisor. Nominations for CADE-20 should be sent by e-mail to

    Robert Nieuwenhuis, CADE-20 Program Chair (roberto@lsi.upc.es), and Tanel Tammet, CADE-20 Conference Chair (tammet@staff.ttu.ee)

    with copies to

    Franz Baader, CADE Inc. President (baader@tcs.inf.tu-dresden.de), and Neil V. Murray, CADE Inc. Treasurer (nvm@cs.albany.edu).

    Nominations must arrive no later than June 8, and the winners will be notified by June 15. The awards will be presented at CADE; if 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 Election

    Amy Felty, AAR and CADE Secretary

    The board of trustees currently includes (in alphabetical order):

  • Franz Baader (President, CADE-19 Program Chair, elected 10/2003)
  • David Basin (IJCAR 2004 co-Program Chair, elected 10/2004)
  • Peter Baumgartner (elected 10/2003)
  • Maria Paola Bonacina (Secretary, 9/1999 to 5/2004, elected 10/2004)
  • Amy Felty (Secretary, appointed 5/2004)
  • Uli Furbach (IJCAR 2006 co-Program Chair)
  • Rajeev Goré (elected 10/2004)
  • Michael Kohlhase (elected 10/2000, reelected 10/2003)
  • Neil Murray (Treasurer)
  • Robert Nieuwenhuis (CADE-20 Program Chair)
  • Geoff Sutcliffe (elected 10/2004)
  • Andrei Voronkov (Vice President, CADE-18 Program Chair, elected 10/2002)
  • Toby Walsh (elected 10/2002)
  • The terms of Andrei Voronkov and Toby Walsh expire after CADE-20, because CADE trustees are elected for three years. The term of office of Robert Nieuwenhuis as program chair of CADE-20 also ends.

    Among the outgoing trustees, Andrei Voronkov and Toby Walsh are eligible to be nominated for a second term. Robert Nieuwenhuis as outgoing ex-officio trustee is also eligible to be nominated for a first term as an elected trustee.

    Nominations can be made by any AAR member, either by e-mail or in person at the CADE-20 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 CADE-20 (July 27, 2005).

    CADE-20: Call for Participation

    The 20th International Conference on Automated Deduction will take place in Tallinn, Estonia, July 22-27, 2005. CADE is the major forum for the presentation of research in all aspects of automated deduction, from logics to methods (e.g., term rewriting, tableaux, model generation) to applications.

    Important Dates:

    Deadline for early registration: June 20, 2005
    Deadline for noncash payments: July 12, 2005
    Workshops: July 22-23, 2005
    Conference: July 24-27, 2005

    Invited talks will be given at CADE-20 by Randal Bryant (CMU), Gilles Dowek (Ecole Polytechnique), and Frank Wolter (U. Liverpool).

    Invited tutorials will be given by Bruno Blanchet on "An Automatic Security Protocol Verifier Based on Resolution Theorem Proving" and by Enrico Giunchiglia on "Beyond SAT: QSAT, and SAT-based Decision Procedures."

    In addition, more than two dozen papers have been accepted for presentation. The papers were selected after a rigorous review process and reflect a wide range of topics, from theory to algorithms to applications.

    Five system descriptions will also be presented.

    In addition, several workshops and tutorials are offered:

  • Workshop on Empirically Successful Classical Automated Reasoning (ESCAR) -- Geoff Sutcliffe, Stephan Schulz, and Bernd Fischer
  • Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING) -- Wolfgang Ahrendt, Peter Baumgartner and Hans de Nivelle
  • Workshop on Constraints in Formal Verification 2005 (CFV'05) -- Joao Marques-Silva, Miroslav Velev
  • Tutorial on Integrating Object-Oriented Design and Deductive Verification of Software -- Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Peter Schmitt
  • For further information see the Web site.

    Organizing Chair: Tanel Tammet (Tallinn TU)
    Workshop and Tutorial Chair: Frank Pfenning (CMU)
    Program Chair: Robert Nieuwenhuis (UPC Barcelona)
    Publicity Chair: Brigitte Pientka (McGill)

    CADE ATP System Competition

    The CADE ATP System Competition will be held at the 20th International Conference on Automated Deduction in Tallin, Estonia, July 26, 2005.

    The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE conference.

    CASC evaluates the performance of sound, fully automatic, classical first-order ATP systems. The evaluation is in terms of the number of problems solved, the number of problems solved with a solution output, and the average runtime for problems solved, 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 is overseen by a panel of knowledgeable researchers who are not participating in the event. The panel members are Uli Furbach, Roberto Nieuwenhuis, and Jeff Pelletier. Further details and registration information are available at the Web site.

    Registration of systems for CASC-20 is now invited. System registration closes on June 1, 2005. Please register early so that adequate resources can be allocated.

    Call for Papers

    Trends in Logic III

    An international conference in memoriam for A. Mostowski, H. Rasiowa, and C. Rauszer will be held in Warsaw on September 23 and in Ruciane-Nida on September 24-25, 2005. The conference will be held under the auspices of Studia Logica, Fundamenta Informaticae, and the Polish Association for Logic and Philosophy of Science. The goals are to gather the former students and collaborators of Andrzej Mostowski, Helena Rasiowa, and Cecylia Rauszer to recall their scientific and methodological heritage; to review the impact of their results on the foundations of mathematics and computer science; and to discuss future developments of logic and its applications.

    Contributions motivated by the research of A. Mostowski, H. Rasiowa, and C. Rauszer or dedicated to them are invited in the following areas: mathematical logic, foundation of mathematics, and mathematical and logical foundations of computer science. Please send an extended abstract not exceeding 6 pages (by e-mail in pdf format) to Wiktor Marek (marek@cs.uky.edu) by June 15, 2005. See also the Studia Logica Web page and the call for papers.


    The 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12) will be held December 2-6, 2005, in Montego Bay, Jamaica. Submission of papers for presentation at the conference is now invited. Topics of interest include the following:

    automated reasoning propositional reasoning
    interactive theorem proving description logics
    proof assistants modal and temporal logics
    proof planning nonmonotonic reasoning
    proof checking constructive logic and type theory
    rewriting and unification lambda and combinatory calculi
    software and hardware verification logic programming
    network and protocol verification constraint programming
    systems specification and synthesis logical foundations of programming
    model checking computational interpretations of logic
    proof-carrying code logic and computational complexity
    logic and databases logic in artificial intelligence
    reasoning over ontologies knowledge representation and reasoning
    reasoning for the semantic web reasoning about actions

    Full and short papers are welcome. Full papers (up to 15 pages) may be either regular papers containing new results, or experimental papers describing implementations or evaluations of systems. Short papers (up to 5 pages) may describe work in progress or provide system descriptions. The full paper proceedings of LPAR-12 will be published by Springer-Verlag in the LNAI series. The short paper proceedings of LPAR-12 will be published by the conference. Papers must be prepared by using the Springer-Verlag instructions for authors.

    Papers must be submitted in plain postscript or PDF format, through the online submission system.

    Dates and Deadlines:

    Submission of full paper abstracts: July 11
    Submission of full papers: July 18

    Questions related to submission may be sent to the program chairs, Geoff Sutcliffe (geoff@cs.maimi.edu) and Andrei Voronkov (voronkov@cs.man.ac.uk).


    The 2006 Federated Logic Conference will take place in Seattle, Washington, August 10-22, 2006.

    The following conferences will participate in FLoC: Int'l Conference on Computer-Aided Verification (CAV), Int'l Conference on Rewriting Techniques and Applications (RTA), IEEE Symposium on Logic in Computer Science (LICS), Int'l Conference on Logic Programming (ICLP), Int'l Conference on Theory and Applications of Satisfiability Testing (SAT), and Int'l Joint Conference on Automated Reasoning (IJCAR).

    Preconference workshops will be held on August 10-11. LICS, RTA, and SAT will be held in parallel on August 12-15, to be followed by mid-conference workshops and excursions on August 15-16. CAV, ICLP, and IJCAR will be held in parallel on August 16-21, to be followed by postconference workshops on August 21-22. Plenary events involving all the conferences are planned.

    Calls for papers and call for workshop proposals will be issued in the near future. For additional information regarding the participating meetings, please check the FLoC Web page.

    Call for Abstracts of Theses

    Since 2000, the AAR Newsletter has published the abstracts of new doctorate theses in automated reasoning. We encourage you to submit your own abstract or to invite your students to submit the information. The abstract should indicate authors and title of the thesis, name of the advisor, date of defense and institution granting the degree, and it should provide a brief summary of the thesis, including its table of contents. Please submit the abstracts to Gail Pieper, AAR Newsletter Editor, at pieper@mcs.anl.gov.

    Gail W. Pieper
    May 2005