AARNEWS - June 2006



No. 71, June 2006

From the AAR President
Boyer, Kaufmann, and Moore Win 2005 ACM Software System Award
Bibel Wins Herbrand Award
Woody Bledsoe Student Travel Award
Call for Nominations: CADE Trustees Election
Satisfiability Modulo Theories Competition
Call for Abstracts of Theses
ESSLLI 2007: Call for Course and Workshop Proposals
Call for Papers: Journal of Logic and Computation Special Issue
Conference Calls for Papers

  • VMCAI'07
  • FLoC-06
  • MICAI 2006
  • LFCS'07
  • TABLEAUX 2007
  • From the AAR President, Larry Wos...

    I am delighted to start this issue of the AAR Newsletter with the announcement of two awards: one to Wolfgang Bibel, and the other to Robert Boyer, Matt Kaufmann, and J Strother Moore. Congratulations to all!

    For those who are now motivated to try for other awards, I mention two that are featured in this issue: a student travel award for FLoC and an SMT competition for CAV'06. Both events will take place in Seattle, Washington, in mid-August.

    Boyer, Kaufmann, and Moore Win 2005 ACM Software System Award

    We are proud to announce that Robert Boyer, Matt Kaufmann, and J Strother Moore have won the ACM Software System Award for 2005 for the development and application of the Boyer-Moore Theorem Prover.

    The Software System Award is given to an institution or individuals recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. The Boyer-Moore Theorem Prover developers were honored ``for pioneering and engineering a most effective theorem prover ... as a formal methods tool for verifying safety-critical hardware and software.''

    The award carries a prize of $10,000 provided by IBM.

    Bibel Wins 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 Wolfgang Bibel is to receive the 2006 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his seminal work on first-order theorem proving and its applications in artificial intelligence and programming.

    His research on the connection method laid the foundations for many modern deduction systems, and it had significant influence on other research areas such as logic programming, knowledge representation, and deductive planning.

    Woody Bledsoe Student Travel Award:
    Call for Nominations

    Peter Baumgartner (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 2006, IJCAR will take place from August 17 through 20, in Seattle, Washington, USA, as part of the Federated Logic Conference (FLoC). For further information see the Web page.

    The winners will be reimbursed (up to some maximum amount to be determined, usually around US$ 500-750) 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, students in other situations are also much encouraged to apply. A nomination consists of a recommendation letter of up to 300 words from the student's supervisor. Nominations for IJCAR 2006 should be sent by e-mail to Peter Baumgartner (Peter.Baumgartner@nicta.com.au) by June 15, 2006. The winners will be notified by June 30 (the early registration deadline for FLoC'06 is July 10). 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 Election
    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):

    The terms of Franz Baader, Peter Baumgartner, and Michael Kohlhase expire after IJCAR 2006, because CADE trustees are elected for three years. The term of office of Uli Furbach as program chair of IJCAR 2006 also ends.

    Among the outgoing trustees, Franz Baader and Peter Baumgartner are eligible to be nominated for a second term. Uli Furbach 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 IJCAR 2006 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 Franz Baader, CADE President (baader@tcs.inf.tu-dresden.de) and Amy Felty, CADE Secretary (afelty@site.uottawa.ca), by the end of IJCAR 2006 (August 21, 2006).

    Call for Benchmarks and Entrants:
    Satisfiability Modulo Theories Competition

    Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT-COMP aims to spur innovation in SMT research by providing a yearly friendly competition for SMT solvers.

    SMT-COMP came out of discussions surrounding the SMT-LIB initiative, an initiative of the SMT community to build a library of SMT benchmarks in a proposed standard format. SMT-COMP helps serve this goal by contributing collected benchmark formulas used for the competition to the library and by providing an incentive for implementors of SMT solvers to support the SMT-LIB format.

    The methodology and the results of the competition will be presented at the end of CAV'06, which will take place in Seattle, Washington, USA, August 16-20, 2006. A more detailed discussion of the competition will take place in a special SMT-COMP meeting the evening of August 20.


    The potential benchmark divisions for this year will include all of the divisions represented last year as well as several new ones. For detailed descriptions of the divisions, refer to the SMT-LIB Web page.

    As with last year, we reserve the right to remove benchmark divisions if we do not receive enough quality benchmarks or enough solvers in a particular division. If you have access to benchmarks in any of these divisions, even if they are not in the SMT-LIB format, please contact one of the organizers (see below).

    Important Dates

    The organizers are Clark Barrett (New York University, barrett@cs.nyu.edu), Leonardo de Moura (SRI International, demoura@csl.sri.com), and Aaron Stump (Washington University in St. Louis, stump@cse.wustl.edu).

    For details on the competition, see the Web page. For more information on the smt-lib format, see the site.

    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.

    ESSLLI 2007: Call for Course and Workshop Proposals

    The 19th European Summer School in Logic, Language and Information (ESSLLI) will take place in Dublin, Ireland, August 6-17, 2007. ESSLLI offers foundational, introductory, and advanced courses, as well as workshops, covering a wide variety of topics in three areas: Language and Computation, Language and Logic, and Logic and Computation.

    Courses are taught by 1 or 2 lecturers. Courses consist of five sessions (a one-week course), each session lasting 90 minutes. Lecturers who want to offer a long, two-week course should structure it as two independent one-week courses (ideally, with an introductory part in the first week of ESSLLI, and a more advanced part during the second). The ESSLLI program committee has the right to select only one of the two proposed courses.

    Timetable for Course Proposal Submission

    Foundational Courses: These are strictly 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 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, for instance, Language and Computation, 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 Ph.D. students. Proposals for advanced courses should specify the prerequisites in detail.

    Workshops: The aim of the workshops is to provide a forum for advanced Ph.D. students and other researchers to present and discuss their work. Workshops should have a well defined theme, and workshop organizers should be specialists in the theme of the workshop. Organizers must give a general introduction to the theme during the first session of the workshop. They are also responsible for the organization and program of the workshop including inviting the submission of papers, reviewing, expenses of invited speakers, and so forth. Each workshop organizer will be responsible for producing the 1st Call for Papers in December 2006. The call must make it clear that the workshop is open to all members of the LLI community. It should also note that all workshop contributors must register for the Summer School.

    Workshop proposals must be submitted by June 15, 2006. Notice that workshop speakers will be required to register for the Summer School; however, they will be able to register at a reduced rate to be determined by the local organizers. A Web-based form for submitting course and workshop proposals is accessible at the Web site.

    Finances: All teaching and organizing at the summer schools is done on a voluntary basis in order to keep the participants' fees as low as possible. Lecturers and organizers are not paid for their contribution but are reimbursed for travel and accommodation (up to a fixed, maximum amount that will be notified to lecturers when courses are accepted). The local organizers highly appreciate it if, whenever possible, lecturers and workshop organizers find alternative funding to cover travel and accommodation expenses. Such issues might be taken into account when selecting courses. We stress that while proposals from all over the world are welcomed, the Summer School cannot guarantee full reimbursement of travel costs, especially from destinations outside Europe.

    Please note the following: If a course is to be taught by two lecturers, a lump sum is reimbursed to cover travel and accommodation expenses for one lecturer. The splitting of the sum is up to the lecturers.

    Chair: Tomaz Erjavec, Jozef Stefan Institute, Jamova 39, SI-1000 Ljubljana, Slovenia (e-mail: tomaz.erjavec@ijs.si; www: http://nl.ijs.si/et/).

    The Web site for ESSLLI 2007 will become operational in the second half of 2006. For this year's summer school, please see the Web site.

    Call for Papers:
    Journal of Logic and Computation Special Issue on Natural Language and Knowledge Representation

    Researchers are cordially invited to submit articles for a special issue of the Journal of Logic and Computation on natural language and knowledge representation.

    Natural language processing (NLP) and the knowledge representation (KR) communities have common goals. They are both concerned with representing knowledge and with reasoning, since the best test for the semantic capability of an NLP system is performing reasoning tasks. Having these two essential common grounds, the two communities ought to have been collaborating, to provide a well-suited representation language that covers these grounds. However, the two communities also have difficult-to-meet concerns. Mainly, the semantic representation (SR) should be expressive enough and take the information in context into account, while the KR should be equipped with a fast reasoning process.

    The main objection against using an SR or a KR is that they need experts to be understood. Nonexperts communicate (usually) via a natural language (NL), and more or less they understand each other while performing a lot of reasoning. An essential practical value of representations is their attempt to be transparent. This will particularly be useful when or if the system provides a justification for a user or a knowledge engineer on its line of reasoning using the underlying KR (i.e., without generating back to NL).

    We all seem to believe that, compared to natural language, the existing knowledge representation and reasoning systems are poor. Nevertheless, for a long time, the KR community has dismissed the idea that NL can be a KR. That's because NL can be very ambiguous and there are syntactic and semantic processing complexities associated with it. However, researchers in both communities have started looking at this issue again. Possibly, it has to do with the NLP community making some progress in terms of processing and handling ambiguity, the KR community realizing that a lot of knowledge is already "coded" in NL and that one should reconsider the way they handle expressivity and ambiguity.

    For this special journal issue of logic and computation, we invite the submission of original, high-quality articles. Topics for this special issue include the following:

    The deadline for paper submissions (max. 20 pages, pdf) is July 31, 2006. For advice on topic, scope, and suitability for the special issue, or to submit papers electronically, please contact Jana Sukkarieh (j.sukkarieh.94@cantab.net). The submission process also will be soon available on the Web.

    The articles will be peer reviewed, and notification for authors will be sent as soon as possible after the date of submission.

    Conference Calls for Papers


    The Eighth International Conference on Verification, Model Checking, and Abstract Interpretation will take place in Nice, France, January 14-16, 2007.

    VMCAI provides a forum for researchers from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods. VMCAI'07 is co-located with the POPL'07 conference.

    The program of VMCAI'07 will consist of invited lectures, tutorials, refereed research papers, and tool demonstrations. Research contributions can report new results as well as experimental evaluations and comparisons of existing techniques. Topics include the following:

    program verification program certification
    model checking debugging techniques
    abstract interpretation abstract domains
    static analysis type systems
    deductive methods optimization

    Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. The proceedings will be published by Springer in the Lecture Notes in Computer Science series.

    The page limit for submissions is 15 pages in Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewer. Formatting style files can be found at the Web site. The submission deadline is September 8, 2006.

    For further information, see the Web site.


    We are pleased to announce the fourth Federated Logic Conference (FLoC'06) to be held in Seattle, Washington, August 10-22, 2006, at the Seattle Sheraton (http://www.easychair.org/FLoC-06/floc-hotel.html). FLoC'06 promises to be the premier scientific meeting in computational logic in 2006. The following conferences will participate in FLoC'06:

    CAV Conference on Computer Aided Verification (Aug 17-20)
    ICLP Int'l Conference on Logic Programming (Aug 17-20)
    IJCAR Int'l Joint Conference on Automated Reasoning (Aug 17-20)
    LICS IEEE Symposium on Logic in Computer Science (Aug 12-15)
    RTA Conference on Rewriting Techniques and Applications (Aug 12-14)
    SAT Int'l Conference on Theory and Applications of
      Satisfiability Testing (Aug 12-15)

    The six major conferences will be accompanied by 41 workshops, held on Aug. 10-11, 15-16, and 21-22.

    The FLoC'06 program includes a keynote session to commemorate the Goedel Centenary, with John Dawson and Dana Scott as speakers; a keynote talk by David Harel; plenary talks by Randy Bryant and David Dill; and several invited talks.

    FLoC has received an NSF grant to provide funds for travel grants of up to $750 for student attendees of FLoC'06. We expect to award about 50 grants. See application information on the Web site.

    Online registration for FLoC is now open at the Web site.

    The deadline for preferred hotel rate is June 21, 2006; the deadline for early registration is July 10, 2006.

    MICAI 2006

    The 5th Mexican International Conference on Artificial Intelligence will take place November 13-17, iin Mexico. Papers accepted for oral presentation will be published by Springer in Lecture Notes in Artificial Intelligence. Papers accepted for poster sessions will be published by IEEE CS Press. Submissions must be received via the Web site by June 2, 2006.


    The Symposium on Logical Foundations of Computer Science will take place in New York City, June 4-7, 2007. The LFCS series provides an outlet for the fast-growing body of work in the logical foundations of computer science, for example, areas of fundamental theoretical logic related to computer science. Topics of particular interest to AAR members include logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; term rewriting; intelligent and multiple agent system logics; logics of proof and justification; and nonmonotonic reasoning.

    Submissions must be made electronically (15 pages, according to LNCS standards) to lfcs07@gmail.com, by December 18, 2006. For more information, see the Web page.

    TABLEAUX 2007

    TABLEAUX 2007, Automated Reasoning with Analytic Tableaux and Related Methods, will take place July 3-6, 2007, in Aix en Provence, France. The PC chair is Nicola Olivetti, LSIS, Paul Cézanne University, Marseille, France.

    Gail Pieper pieper@mcs.anl.gov
    June 2006