NEWSLETTER No. 74, January 2007

From the AAR President
Herbrand Award: Call for Nominations
Call for Papers

  • CADE-21
  • MKM 2007
  • Trends in Logic V
  • TABLEAUX 2007
  • ASL European Summer Meeting
  • HyLo 2007
  • FTP'07
  • From the AAR President, Larry Wos...

    This issue comes earlier than usual in the new year because we have several important announcements with early deadlines. Of especial interest are the Herbrand Award, for experienced researchers who have made major contributions to automated reasoning, and the Woody Bledsoe Student Travel Award, for students new to the fields of mathematics, AI, and automated theorem proving.

    Herbrand Award:
    Call for Nominations

    Amy Felty
    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)
    Mark E. Stickel (2002)
    Peter B. Andrews (2003)
    Harald Ganzinger (2004)
    Martin Davis (2005)
    Wolfgang Bibel (2006)

    A nomination is required for consideration for the Herbrand award, which will be given at CADE 2007. The deadline for nominations for the Herbrand Award is March 15, 2007.

    Nominations pending from previous years must be resubmitted in order to be considered.

    Nominations should consist of a letter (preferably e-mail) 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

    Franz Baader
    President of CADE Inc.
    with copies to

    Call for Papers


    The 21st International Conference on Automated Deduction will be held at the International University, Bremen, Germany July 17-20, 2007, with workshops on July 15-16.

    CADE is the major forum for the presentation of research in all aspects of automated deduction:

    Invited Speakers:

    Peter Baumgartner, NICTA and Australian National University
    Rustan Leino, Microsoft Research
    Colin Stirling, University of Edinburgh
    Ashish Tiwari, SRI International

    Affiliated Workshops (July 15-16, 2007):

    ADDCT - Automated Deduction: Decidability, Complexity, Tractability
    CVF - Fourth International Workshop on Constraints in Formal Verification
    DISPROVING - Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability
    ESARLT - Empirically Successful Automated Reasoning in Large Theories (see the call in this newsletter)
    ISABELLE-WS - Isabelle Workshop
    LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
    VERIFY - 4th International Verification Workshop

    Paper Submission:

    Submission is electronic in PostScript or PDF format via the EasyChair system. Submitted papers must conform to the Springer LNCS style, preferrably using LaTeX2e and the Springer llncs class files available on the Web. Submissions can be full papers, for work on foundations, applications, or implementation techniques (15 pages), as well as system descriptions (5 pages), for describing publicly available systems. The proceedings will be published in the Springer LNCS series. Submissions are now open via EasyChair. Titles and abstracts are due February 16, 2007. Full papers are due February 23, 2007.

    The conference chair is Michael Kohlhase (IUB); the workshop and tutorial chair is Christoph Benzmueller (Cambridge); the program chair is Frank Pfenning (CMU).

    Woody Bledsoe Student Travel Award:

    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.

    The winners of the 2007 Travel Award will be partially reimbursed for their conference registration, transportation, and accommodation expenses. Past awards have varied but have typically been 150-600 Euro, depending on the degree of active participation and the distance that needs to be traveled. 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 CADE-21 should be sent by e-mail to Michael Kohlhase, CADE-21 Conference Chair ( Nominations must arrive no later than June 1, 2007; the winners will be notified by June 10. The awards will be presented at CADE. In case a winner does not attend, the chairs and trustees may transfer the award to another nominee or give no award.


    The CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (ESARLT) will bring together practitioners and researchers who are concerned with the development and application of automated reasoning in large theories--theories in which there are

    In large theories it is useful to develop and apply intelligent reasoning techniques that go beyond ``black box'' reasoning, to include techniques for selecting axioms, and using proved theorems as lemmas. Reasoning in all forms (automated, interactive, etc.) and all logics (classical, nonclassical, all orders, etc.) is of interest to the workshop. The workshop will discuss only ``really running" systems and applications, and not theoretical ideas that have not yet been translated into working software.

    ESARLT is the successor to the successful ESFOR, ESCAR, ESHOL, and ESCoR workshops. CADE-21 will be July 15-20, 2007.

    Submission of papers for presentation at the workshop, and proposals for system and application demonstrations at the workshop, are invited. Submissions will be refereed, and a balanced program of high-quality contributions will be selected. The selected contributions will be printed as workshop proceedings and will also be published electronically. The submission deadline is May 7, 2007, notification of acceptance is on June 8, and final versions are due June 25. Submission information is online.

    MKM 2007

    The Sixth International Conference on Mathematical Knowledge Management will be held in Hagenberg, Austria, June 27-30, 2007.

    Mathematical knowledge management is an innovative field in the intersection of mathematics and computer science. Its development is driven on the one hand by the new technological possibilities that computer science, the Internet, and intelligent knowledge processing offer, and on the other hand by the need for new techniques for managing the rapidly growing volume of mathematical knowledge.

    The conference is concerned with all aspects of mathematical knowledge management, including the following of particular interest to AAR members:

    The deadline for submissions is February 12, 2007. Submitted papers should not exceed 15 pages and must be original. The proceedings will be published in the Springer-Verlag series Lecture Notes in Artificial Intelligence. Authors of accepted papers are expected to present their work at the conference.

    The local organizer is Wolfgang Windsteiger (Johannes Kepler University, Linz, Austria). For more information, see the MKM Interest Group or Calculemus 2007 Web sites.

    Note that there will be affiliated workshops with the MKM and Calculemus conferences. Those interested in organizing a workshop should contact the co-chairs Manfred Kerber and Robert Miner at

    Trends in Logic V

    Trends in Logic V, a Studia Logica international conference, will take place in Guangzhou, China, July 6-9, 2007. The conference seeks to bring together researchers working in many-valued logics, encourage a greater degree interaction among the featured research communities, and act as a catalyst for new directions of research. Contributions are welcome that concern applications of mathematical methods to philosophical problems, especially in the following areas:

    Contributors should send an abstract not exceeding two pages to Jacek Malinowski ( by April 1, 2007. Abstracts must be submitted as Latex or MS Word files. Authors will be notified about acceptance before May 15, 2007.

    For further information, contact the Institute of Logic and Cognition, Sun Yat-sen University (the south campus), Guangzhou, China, 510275; fax: +86 20 8411 0298; e-mail

    See also the general Studia Logica Web site and the online call for papers.

    TABLEAUX 2007

    The 16th international meeting on Automated Reasoning with Analytic Tableaux and Related Methods will be held in Aix en Provence, France, July 3-6, 2007.

    Tableau methods are a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis. The conference brings together researchers interested in the theoretical foundations, implementation techniques, systems development, and applications of the mechanization of reasoning with tableaux and related methods. Topics include the following:

    Of particular interest are papers describing applications of tableaux and related methods in areas such as hardware and software verification, knowledge engineering, and the semantic Web.

    Submissions are invited in four categories:

    Submissions in categories A and B will be reviewed by peers, typically members of the program committee. Accepted papers in these categories will be published in the conference proceedings. For category B submissions a working implementation must exist and be available to the referees.

    Submissions in category C will be reviewed by members of the program committee, and a collection of the accepted papers in this category will be published as a technical report of the LSIS/Université Paul Cézanne.

    Tutorial submissions in category D may be at introductory, intermediate, or advanced levels. Novel topics and topics of broad interest are preferred. The submission should include the title, the author, the topic of the tutorial, its level, its relevance to conference topics, and a description of the interest and the scientific contents of the proposed tutorial. Tutorial proposals will be reviewed by members of the program committee.

    The deadline for submission of title and abstract is February 2, 2007. Paper submissions are due February 9, 2007. Authors of accepted papers are expected to present their work at the conference.

    Workshops TABLEAUX 2007 also has launched a call for workshop proposals on specialized subjects in the range of the conference topics. Up to two proposals can be accepted. The purpose of a workshop is to offer an opportunity of presenting novel ideas, ongoing research, and to discuss the state of the art of an area in a less formal but more focused way than the conference itself. It is also a good opportunity for young researchers to present their own work and to obtain feedback. The format of a workshop is left to the organizers, but it is expected to contain significant time for discussion. The intended schedule is for one-day workshops. The deadline for workshop proposal submissions is January 31, 2007.

    For more information, see the Web site.

    2007 ASL European Summer Meeting

    The Logic Colloquium '07 will take place in Wroclaw, Poland, July 13-19, 2007. This meeting will be collocated with the 2007 International Colloquium on Automata, Languages and Programming (ICALP 2007; see the ASL "other meetings" Web page and the EATCS Web page) and the Twenty-Second Annual IEEE Symposium on Logic In Computer Science (LICS 2007; see the ASL "other meetings" Web page and LICS Web page). Abstracts of contributed talks submitted by ASL members will be published in the Bulletin of Symbolic Logic if they satisfy the rules for abstracts.

    Abstracts--hard copy or e-mail--should be received before the deadline of April 17, 2007. See the ASL Web site for more information.

    HyLo 2007

    The International Workshop on Hybrid Logic 2007 (affiliated with ESSLLI 2007) will be held in Dublin, August 6-10, 2007.

    Hybrid logic is a branch of modal logic allowing direct reference to worlds, times, and states. The expressive power from hybrid logic is useful for applications. Moreover, hybrid-logical machinery improves the behavior of the underlying modal formalism.

    The topic of HyLo 2007 is not only standard hybrid-logical machinery such as nominals, satisfaction operators, and the downarrow binder, but also extensions of modal logic that increase its expressive power. HyLo 2007 Is intended for people interested in description logic, feature logic, applied modal logics, temporal logic, and labeled deduction.

    The submission deadline is March 8, 2007. For Submission details, see the HyLo Web page. Accepted papers will appear in the workshop proceedings published by ESSLLI. Revised versions of accepted papers will be published in a special issue of Journal of Logic, Language and Information.


    The International Workshop on First-Order Theorem Proving (FTP'07) will be held in Liverpool, England, September 12-13, 2007. The workshop will be collocated with the 6th International Symposium on Frontiers of Combining Systems (FroCos'07), which will take place prior to FTP'07. The FTP workshop focuses on all aspects of theorem proving in first-order logic. It aims to be a forum for the presentation of original work and for the discussion of work in progress. Relevant topics for the workshop include the following:

  • Theorem proving in first-order classical, many-valued, and modal logics, including satisfiability in propositional logic, satisfiability modulo theories, decision procedures, constraint reasoning, equational reasoning, term rewriting, resolution, and paramodulation/superposition
  • Strategies and complexity of theorem proving procedures
  • Applications of first-order theorem proving to program verification, model checking, artificial intelligence, mathematics, and computational linguistics
  • Authors are invited to submit papers in the following categories:
  • Extended abstracts of 5-10 pages describing original results, work in progress, or future directions of research.
  • System descriptions of up to 5 pages, describing new systems or significant upgrades of existing ones, especially including experiments; sources and manuals of systems will have to be freely available online
  • Authors are encouraged to use LaTeX and the standard article class/style file (10pt or 11pt). The first page should contain the title, the authors' names, e-mail and postal addresses. Submissions should be made via
    Easychair. The deadline for abstract submission i May 7, 2007. Full papers are due May 14, 2007. Submissions will be reviewed by at least two referees and will be evaluated on their significance, technical merit, and relevance to the workshop. Accepted submissions will be published as a technical report of the University of Liverpool and will be distribted at the workshop. They will also be available on the Web. In addition, a journal special issue is planned after the workshop; the submission will be open to papers on first-order theorem proving.

    For more information about FTP, its scope and previous workshops, please, see the workshops Web page. For regular updates about the workshop organization, please see the FTP'07 Web page. To contact the PC chair, please send an email to Silvio.Ranise[AT] (substitute [AT] with "@").

    Gail Pieper
    January 2007