NEWSLETTER No. 79, January 2008

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

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!

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:

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:

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)unisi.it.

IJCAR

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 http://www.springer.de/comp/lncs/authors.html. 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 www.aslonline.org/studenttravelawards.html for details.

For further information, see the Web.

TCS-2008

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.

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) cs.cmu.edu, or Robert P. Kurshan, Cadence, rkurshan (at) cadence.com. 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.

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.

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.

For further information, see the Web.

For further information, see the Web site.

For more information, visit the Web site.