NEWSLETTER No. 79, January 2008

From the AAR President
Call for Nominations for Herbrand Award
Call for Papers, Workshops, and Posters

  • RTA 2008
  • TIME 2008
  • Logic, Algebra and Truth Degrees 2008
  • IJCAR 2008
  • WoLLIC 2008
  • TCS-2008

  • Call for Award Nominations
  • CAV Award
  • Ackermann Award 2008

  • Book Announcement
    Special Issue on Hybrid Logic
    RISC Summer 2008
    LEO-II: An Automated Theorem Prover for Higher-Order Logic
    Call for Position Papers Exploiting Concurrency Efficiently and Correctly

    From the AAR President, Larry Wos...
    This marks the 25th year the AAR Newsletter has been in existence. I am indeed amazed, on the one hand, how far the field of automated reasoning has come and, on the other hand, how much more remains to be done. We have, for example, solved long-standing open questions in mathematics and logic. But some would argue that we have not completed automating our automated reasoning programs. While both points are true, I happen to be one who does not looks forward to complete automation, perhaps for a selfish reason: It would take the fun out of my experimentation with diverse parameters!

    I was interested to learn that in the December 2007/January 2008 issue of Innovation, in an article "Will Computers Think Like Humans?" Jeff Hawkins comments that he felt "the field of AI was heading down the wrong path." Long ago, when I became interested in automated reasoning, I felt that way -- and I still do. Hawkins has decided to investigate the human brain. We who are fascinated with automated reasoning have attacked the problem in a different manner. Perhaps this year will lead to major successes for us all!

    Call for Nominations for Herbrand Award
    Wolfgang Ahrendt
    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)
    Alan Bundy (2007)

    A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2008 is March 14, 2008.

    Nominations pending from previous years must be resubmitted in order to be considered. Nominations should consist of a letter (preferably email) 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

    RTA 2008

    The 19th International Conference on Rewriting Techniques and Applications (RTA 2008) is organized as part of the RISC Summer 2008, which comprises five conferences, five workshops, and the Training School in Symbolic Computation and is followed by the 3rd International School on Rewriting in Obergurgl. RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include the following:

  • Applications: case studies; analysis of cryptographic protocols; rule-based (functional and logic) programming; symbolic and algebraic computation; theorem proving; system synthesis and verification; proof checking; reasoning about programming languages and logics; program transformation;
  • Foundations: matching and unification; narrowing; completion techniques; strategies; rewriting calculi, constraint solving; tree automata; termination; combination;
  • Frameworks: string, term, and graph rewriting; lambda-calculus and higher-order rewriting; constrained rewriting/deduction; categorical and infinitary rewriting; integration of decision procedures;
  • Implementation: implementation techniques; parallel execution; rewrite tools; termination checking;
  • Semantics: equational logic; rewriting logic; rewriting models of programs.
  • Submission categories include regular research papers (15 pages) and system descriptions (10 pages); problem sets and submissions describing interesting applications of rewriting techniques are also welcome. Papers must be submitted electronically through the EasyChair system. Abstracts are due February 4, 2008; the paper submission deadline is February 11, 2008.

    An award will be given to the best paper or papers as decided by the program committee.

    Limited student support will be available and announced in future versions of this call.

    TIME 2008 - 15th International Symposium on Temporal Representation and Reasoning

    TIME 2008 will take place in Montreal, Canada, June 16-18, 2008. The symposium aims to bring together researchers from distinct research areas involving the management of temporal data as well as the reasoning about temporal aspects of information. This unique and well-established event further has as its objectives to bridge theoretical and applied research, as well as to serve as an interdisciplinary forum for exchange among researchers from the areas of artificial intelligence, database management, logic and verification, and beyond. TIME 2008 encompasses three tracks, but has a single program committee. The conference will span three days, and will be organized as a combination of technical paper presentations, poster sessions, and keynote talks.

    Topics that fit the interests of the symposium include those of the following tracks: Track 1: Temporal Representation and Reasoning in AI, Track 2: Temporal Database Management, and Track 3: Temporal Logic and Verification in Computer Science.

    Submitted papers will be refereed by at least three reviewers for quality, correctness, originality, and relevance. Accepted papers will be presented at the symposium and included in the proceedings, which will be published by the IEEE Computer Society Press.

    Paper submission deadline is January 11, 2008. For further information see the Web.

    Logic, Algebra and Truth Degrees 2008

    The Logic, Algebra and Truth Degrees meeting will take place September 8-11, in Siena, Italy. This is the first official meeting of the recently founded EUSFLAT Working Group on Mathematical Fuzzy Logic.

    Mathematical fuzzy logic is a subdiscipline of mathematical logic, which studies the notion of comparative truth. The assumption that "truth comes in degrees" has proved useful in many areas of mathematics, computer science, and philosophy, both theoretical and practical. The goal of this meeting is to foster collaboration between researchers in the area of mathematical fuzzy logic and to promote communication and cooperation with members of neighboring fields.

    The featured topics include the following:

  • Proof systems for fuzzy logics: Hilbert, Gentzen, natural deduction, tableaux, resolution, computational complexity, etc.
  • Algebraic semantics: residuated lattices, MTL-algebras, BL-algebras, MV-algebras, abstract algebraic logic, functional representation, etc.
  • Game-theory: Giles games, Renyi-Ulam games, evaluation games, etc.
  • First-order fuzzy logics: axiomatizations, arithmetical hierarchy, model theory, etc.
  • Higher-order fuzzy logical systems: type theories, fuzzy class theory, and formal fuzzy mathematics.
  • Extended fuzzy logical systems: adding modalities or truth constants, "dynamification," evaluated syntax, etc.
  • Philosophical issues: connections with vagueness and uncertainty.
  • Applied fuzzy logical calculi: foundations of fuzzy logical programming, logic-based reasoning about similarity, fuzzy description logics, etc.
  • Those interested in presenting a paper should submit a 1-2 page abstract at the Web site. Submissions will be confirmed automatically on the e-mail address you provide. The accepted abstracts will be available on-line after the final decision of the program committee.

    The deadline for contributions is April 30, 2008. Notification of acceptance/rejection will be sent by June 30, 2008.

    Authors of the best contributions will be invited to submit a paper based on the presentation to a special issue in a mathematical logic journal. Details on the special issue will be distributed at a later point by the editors.

    For further information please visit the official Web page of the conference. All correspondence should be directed to latd2008(at)


    IJCAR 2008 , the 4th International Joint Conference on Automated Reasoning, will take place in Sydney, Australia. IJCAR is the premier international joint conference on all aspects of automated reasoning, including foundations, implementations, and applications. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions and invited talks. There will be two days of workshops and tutorials, August 10-11, and the conference, August 12-15.

    IJCAR 2008 invites submissions related to all aspects of automated reasoning, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited. See the IJCAR website for a detailed list of logics, methods, and applications of interest. The proceedings of IJCAR 2008 will be published by Springer-Verlag in the LNAI/LNCS series. Submission is electronic, through the Web. Authors are strongly encouraged to use LaTeX and the Springer "llncs" format, which can be obtained from The page limit is 15 pages for full papers and 5 pages for system descriptions. The paper registration deadline is February 22, 2008; the paper submission deadline is March 3, 2008.

    WoLLIC 2008

    The 15th Workshop on Logic, Language, Information and Computation will be held in Edinburgh, Scotland, from July 1-4, 2008. WoLLIC is an annual international forum on interdisciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection. Proposed contributions must not exceed 10 pages (in font 10 or higher), with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. Papers must be submitted electronically on the Web. A title and single-paragraph abstract should be submitted by February 24, and the full paper by March 2 (firm date).

    The proceedings of WoLLIC 2008, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's Lecture Notes in Computer Science (tbc). In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published as a special post-conference WoLLIC 2008 issue of the Journal of Logic and Computation (tbc).

    ASL sponsorship of WoLLIC 2008 will permit ASL student members to apply for a modest travel grant (deadline: April 1, 2008). See for details.

    For further information, see the Web.


    The 5TH IFIP International Conference on Theoretical Computer Science (TCS-2008) will be held in conjunction with the 20th IFIP World Computer Congress on September 7-10, 2008, in Milan, Italy. Submission of papers will be in two stages: a short abstract due on February 8, 2008, and the 12-page paper due February, 15, 2008. The results of the paper must be unpublished and not submitted for publication elsewhere, including journals and the proceedings of other symposia or workshops. Authors will be notified of acceptance or rejection via e-mail by March 31. One author of each accepted paper should present it at the conference.

    TCS2008 will be composed of two distinct, but interrelated tracks: Track A on Algorithms, Complexity and Models of Computation, and Track B on Logic, Semantics, Specification and Verification.

    The proceedings will be published by SSBM (Springer Science and Business Media). Submissions, as well as final versions, are limited to 12 pages, in the final SSBM format. The instructions for preparing the papers can be downloaded from the Web or by ftp. Only electronic submissions will be accepted, via Track A or Track B. February 8, 2008, is the abstract submission deadline. February 15, 2008, is the 12-page paper submission deadline.

    ESSLLI 2008

    The Student Session of the 20th European Summer School in Logic, Language and Information will be held in Hamburg, Germany, on August 4-15, 2008. The aim of the student session is to give an opportunity to students at all levels (Bachelor-, Master- and PhD-students) to present and discuss their work in progress with a possibility to get feedback from senior researchers. Each year, 18 papers are selected for oral presentation and a number of others for poster presentation.

    The program committee invites submissions of papers (up to 7 pages including references) for oral and poster presentation and for appearance in the proceedings. We welcome submissions with topics within the areas of logic, language, and computation. Submission deadline is February 15, 2008.

    The ESSLLI Student Session encourages submissions from students at any level, undergraduates as well as postgraduates. Papers coauthored by nonstudents will not be accepted. The papers should describe original, unpublished work, completed or in progress, that demonstrates insight, creativity, and promise. No previously published papers should be submitted.

    The preferred formats of submissions are PostScript or PDF, although other formats will also be accepted. More submission details and all relevant information at the Web site.

    Call for Award Nominations

    CAV Award

    An annual award, called the CAV Award, has been established "for a specific fundamental contribution or a series of outstanding contributions to the field of Computer-Aided Verification." The cited contribution(s) must have been made not more recently than five years ago and not over twenty years ago. In addition, the contribution(s) should not yet have received recognition via a major award, such as the ACM Turing or Kanellakis Awards.

    The award of $10,000 will be granted to an individual or a group of individuals chosen by the Award Committee from a list of nominations. The Award Committee may choose to make no award in a given year.

    The CAV Award will be presented in an award ceremony at the Computer-Aided Verification Conference and a citation will be published in a journal of record (currently, Formal Methods in System Design).

    Anyone, with the exception of members of the Award Committee, is eligible to receive the Award. Anyone can submit a nomination except a member of the Steering Committee of the Computer-Aided Verification Conference, or someone whose term of service on the Award Committee ended within the last two years. The Award Committee can originate a nomination.

    A nomination must state clearly the contribution(s), explain why the contribution is fundamental or the series of contributions is outstanding, and be accompanied by supporting letters and other evidence of worthiness. Nominations should include a proposed citation (up to 25 words), a succinct (100-250 words) description of the contribution(s), and a detailed statement to justify the nomination.

    For the CAV Award in 2008, please send nominations to one of the following two Steering Committee members of the Computer-Aided Verification Conference, who will forward the nominations to the Chair of the Award Committee: Edmund M. Clarke, CMU, emc (at), or Robert P. Kurshan, Cadence, rkurshan (at) Nominations must be received by January 28, 2008.

    Ackermann Award 2008

    Nominations are sought for the 2008 Ackermann Award for Ph.D. dissertations in topics specified by the EACSL and LICS conferences. The dissertation must have been formally accepted as a Ph.D. thesis at a university or equivalent institution between Jan. 1, 2006, and December 31, 2007. Submission details are available on the Web. The deadline for submission is January 15, 2008.

    The award consists of a diploma, an invitation to present the thesis at the CSL conference, the publication of the abstract of the thesis and the laudation in the CSL proceedings, and travel support to attend the conference.

    The 2008 Ackermann Award will be presented to the recipients at the annual conference of the EACSL (CSL'08). The jury is entitled to give more than one award per year. Previous Ackermann Award recipients were the following: 2005: Mikolaj Bojanczyk, Konstantin Korovin, Nathan Segerlind; 2006: Stefan Milius and Balder ten Cate; and 2007: Dietmar Berwanger, Stephane Lengrand and Ting Zhang. For 2007-2009, the Award is sponsored by Logitech, S.A., Romanel, Switzerland, the world;s leading provider of personal peripherals.

    Book Announcement

    A new textbook titled The Calculus of Computation: Decision Procedures with Applications to Verification by Aaron R. Bradley and Zohar Manna has been published by Springer (366 pages, ISBN: 978-3-540-74112-1). Written for graduate and advanced undergraduate students, this textbook introduces computational logic from the foundations of first-order logic to state-of-the-art decision procedures for arithmetic, data structures, and combination theories. It also presents a logical approach to engineering correct software. Verification exercises, supported by free software, develop the reader's facility in specifying and verifying software using logic. The treatment of verification concludes with an introduction to the static analysis of software. Further information can be found at the Web.

    Special Issue on Hybrid Logic

    Guest editors Torben Brauner and Thomas Bolander have issued a call for contributions to a special issue on hybrid logic, to be published in the Journal of Logic, Language and Information. Hybrid logic is a branch of modal logic allowing direct reference to worlds/times/states. It is easy to justify interest in hybrid logic on applied grounds, because of the usefulness of the additional expressive power. In addition, hybrid-logical machinery improves the behavior of the underlying modal formalism. For example, it becomes far simpler to formulate modal tableau, resolution, and natural deduction in hybrid logic, and completeness and interpolation results can be proved of a generality that is not available in orthodox modal logic. Topics of interest include not only standard hybrid-logical machinery like nominals, satisfaction operators, and the downarrow binder, but generally extensions of modal logic that increase its expressive power. Submission deadline is March 1, 2008.

    RISC Summer 2008

    A series of international scientific events will be held July and August 2008 at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. The events will consist of the following conferences and schools:

  • The 3rd RISC/Science Training School in Symbolic Computation. July 7-20, 2008, RISC, Castle of Hagenberg, Austria.
  • SCSS 2008. Austrian-Japan Workshop on Symbolic Computation in Software Science. July 12-13, 2008, RISC, Castle of Hagenberg, Austria.
  • RTA 2008. The 19th International Conference on Rewriting Techniques and Applications. July 14-18, 2008, RISC, Castle of Hagenberg, Austria.
  • ISSAC 2008. International Symposium on Symbolic and Algebraic Computation. July 20-23, 2008, RISC, Castle of Hagenberg, Austria.
  • SFB-SC 2008. Final Conference of the Special Research Area "Scientific Computing". July 24-26, 2008, RISC, Castle of Hagenberg, Austria.
  • Aldor & Axiom Workshop 2008. July 24-26, 2008, RISC, Castle of Hagenberg, Austria.
  • ACA 2008. The 14th International Conference on Applications of Computer Algebra. July 27-30, 2008, RISC, Castle of Hagenberg, Austria.
  • AB 2008. The 3rd International Conference on Algebraic Biology. July 31-August 2, 2008, RISC, Castle of Hagenberg, Austria.
  • For further information, see the Web.

    LEO-II: An Automated Theorem Prover for Higher-Order Logic

    LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic such as first-order and propositional logic. Currently LEO-II cooperates with the first-order automated theorem provers E, SPASS, and Vampire. LEO-II comes with an automatic and an interactive mode.

    LEO-II is implemented in Objective Caml and its problem representation language is TPTP THF. The distribution contains approx. 70 example problems encoded in TPTP THF syntax.

    The development of LEO-II has been supported by the EPSRC grant EP/D070511/1 at Cambridge University. The people behind the LEO-II system are: C. Benzmueller, L. Paulson, A. Fietzke and F. Theiss from Cambridge University and Saarland Universit

    For further information, see the Web site.

    Call for Position Papers Exploiting Concurrency Efficiently and Correctly

    Our ability to effectively harness the computational power of the next generation of multiprocessor and multicore architectures is predicated upon advances in programming languages and tools for developing concurrent software. This has resulted in a surge of concurrency-related research activity from different viewpoints, such as rethinking of programming abstractions and memory models; standardization and formalization of commonly used APIs (e.g., MPI, OpenMP); and new forms of hardware support for parallel processing.

    While developing tools for verifying and debugging concurrent systems has been an important theme at CAV, we believe that formal methods research can go beyond checking existing code/systems, and play a role in identifying the "right" abstractions for concurrency. The goal of the CAV 2008 Workshop is to bring together CAV researchers with experts who are involved in developing multicore architectures, programming languages, and concurrency libraries.

    The workshop will take place at Princeton, N.J., on July 7-8, 2008. The two-day workshop will include five invited talks and several panel sessions. Authors of position papers will be given an opportunity to present their ideas either as a short presentation or as a poster. A booklet consisting of all the position papers will be distributed to the workshop participants.

    We seek submissions of position statements of 2-4 pages. Possible themes for a position paper include a survey of the authors' relevant recent research, a discussion of deficiencies in current languages and tools, challenges for future verification research, and/or a vision for change. Submissions on all topics relevant to the workshop title are welcome, including the following:

  • Transactional memory
  • Programming constructs for concurrency
  • Formalization of concurrency libraries
  • Verification tools
  • Hardware support for correctness
  • Introducing concurrency in education
  • Of particular interest are position statements from those engaged in significant case studies. The submission deadline is April 10, 2008. The title and the name of the authors should appear at the top of the first page. Email this PDF document to The position papers will be compiled into a booklet that will be handed out to all workshop participants on the first day of the workshop. The papers will not be published.

    At least one author of each position paper is expected to register and attend to present the paper.

    For more information, visit the Web site.

    Gail Pieper
    January 2008