AARNEWS - October 2006



No. 72, October 2006

From the AAR President
Announcement of CADE Elections
Abstract of Recent Ph.D. Thesis in AR
FMCAD 2006: Call for Participation
Logic Summer School
Call for Papers

  • Rewriting Techniques and Applications
  • CiE 2007
  • LICS 2007
  • WoLLIC'2007
  • TABLEAUX 2007

  • Special Issues
  • SMT
  • Computer Security: Foundations and Automated Reasoning
  • From the AAR President, Larry Wos...

    In reading the statements from the four CADE candidates, I was struck by two items. First is the repeated mention of the many smaller, and often competing, subcommunities that have been spawned. I am delighted that automated reasoning has expanded so greatly since the early 1980s. But, like the candidates, I am concerned that the field of automated reasoning itself remains well recognized. And this comment leads to my second point: I note that CADE continues to receive high praise and that each candidate not only believes automated reasonoing remains important but has a clear vision about CADE's role with IJCAR. I encourage AAR members to read each candidate's statement carefully and take the time to vote.

    Announcement of CADE Elections
    Amy Felty
    (Secretary of AAR and CADE)
    E-mail: afelty@site.uottawa.ca

    An election of CADE trustees will be held soon, and all AAR members will receive a ballot. The following people are currently serving as trustees of CADE Inc.:

    Franz Baader (President, CADE-19 Program Chair, elected 10/2003)
    David Basin (IJCAR 2004 Program Co-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 Program Co-chair)
    Rajeev Goré (elected 10/2004)
    Reiner Haehnle (Vice President, elected 10/2005)
    Michael Kohlhase (elected 10/2000, reelected 10/2003)
    Neil Murray (Treasurer)
    Frank Pfenning (CADE-21 Program Chair)
    Geoff Sutcliffe (elected 10/2004)
    Cesare Tinelli (elected 10/2005)

    The terms of Franz Baader, Peter Baumgartner, Uli Furbach, and Michael Kohlhase are expiring. The position of Uli Furbach is taken by Frank Pfenning as CADE-21 program chair. Thus, there are three positions to fill.

    The following candidates were nominated, and their statements are below:

    Statement by Franz Baader

    CADE is the major forum for discussing all aspects of automated reasoning research (theory, implementation, and applications). While theoretical work and work on implementations are very well represented at CADE (through regular papers, system descriptions, and the system competition), we must continue our work on attracting more papers on applications, which are now often published at conferences related to the application area (like CAV, KR).

    In order to ensure the role of CADE as the flagship of automated reasoning, we must try both to keep the high scientific standards of the conference and to attract more automated reasoning-related research from other areas (like knowledge representation, constraint solving, verification, and computer algebra). Another important point is to avoid a fragmentation of the field into many small and specialized subcommunities with their own small conferences and workshops. This does not mean that I am against having these smaller events as well. But there should be one big event (every 2-3 years) where the whole automated reasoning community meets and with which it identifies. For this reason, I am strongly in favour of continuing the IJCAR series and of CADE/IJCAR's participation in the FLoC conferences.

    As CADE president and head of the IJCAR steering committee, I have tried to get more AR-related conferences involved in IJCAR (see, e.g., the participation of TPHOLs in IJCAR'06) and would like to continue these attempts in the future. I also think that our decision to go into FLoC'06 as IJCAR rather than CADE was a good one since it made IJCAR the second-largest conference (w.r.t. number of participants) within FLoC. An important next step is to find a schedule for IJCAR and FLoC that allows for a regular participation of IJCAR within FLoC, while also keeping the identity of the IJCAR constituent meetings, and in particular the role of CADE as the flagship of automated reasoning research.

    Statement by Peter Baumgartner

    My research area is automated deduction, with a focus on automated theorem proving in classical first-order logic and applications. CADE is the main conference for me: I have attended CADE regularly since 1990, co-authored several IJCAR or CADE papers, given a tutorial, and co-organized several workshops at CADE, and our systems participate(d) in CASC. I was the publicity chair of IJCAR in 2001, the workshop chair of IJCAR 2004 and served on the programme committee of CADE and IJCAR. I was the president of the FTP steering committee, and I am an (outgoing) member of the Tableaux Steering committee. Since 2003 I have been serving on the CADE board of trustees.

    I think it is important to address the fragmentation of the field of automated deduction. From the CADE perspective I am consequently very much in favour of co-locating CADE with related conferences, having CADE part of FLoC or integrating it into IJCAR on a regular basis. I would like to see CADE to be more attractive for papers that are often sent to KR, CAV or SAT but are within the scope of CADE, in particular papers about applications of automated deduction technology in these areas.

    Statement by Chris Benzmueller

    For more than a decade I have been an active and fascinated researcher in automated deduction, and my first papers on extensional higher-order theorem proving were presented at the 1998 CADE conference. I consider symbolic reasoning and in particular automated deduction a core challenge of AI, and I think that our field is currently not appropriately positioned in the AI community. Automated deduction plays an important role for proof (semi-)automation in modern proof assistants and mathematics assistance systems (such as our OMEGA system), and these systems in turn share many characteristics of large AI systems in general. While the fragmentation of the research in AI in the past decades, which was mirrored in the field of automated deduction, had a very positive effect on the growing-up of its subareas, I believe that the next decade should foster a mutual fertilization and reintegration. I am glad to see that this process has started. The scope of CADE has become wider over the last years, and CADE is a driving force behind IJCAR.

    Statement by Aaron Stump

    Are the glory days of automated reasoning behind us? Have all the interesting technical problems been solved, and all the worthwhile application areas fully explored? Is the field doomed to a lingering death by inches of incrementality and irrelevance?

    You can count me in the ranks of those who say, absolutely not! I believe that automated reasoning is crucial to the future of both computer science and mathematics. When the Semantic Web is running with description logic ontologies debugged using first-order provers, then we can consider the work done. When proof assistants are routinely used by mathematicians to develop their theories, and by programming language designers to design, verify, and implement their languages, then perhaps we can ponder the twilight of our field. And until program verification based on a combination of manual proof and automation is the industrial common practice, there are still plenty of important problems to help drive both the practical and the theoretical work of the field.

    My own primary interest is in AR techniques for program verification. As I have learned more about AR, I have been drawn to other subfields: SMT solvers (I am a co-organizer of the annual Satisfiability Modulo Theories Competition SMT-COMP, and a regular PC member of the SMT workshop PDPAR), logical frameworks and type theory (CADE 2002 and 2003, JAR 2003), term rewriting and completion (RTA 2005 and 2006), and most recently, proof assistants (I am applying Coq to reason about programming language semantics). I served as a PC member for CADE 2005 and IJCAR 2006, and I am on the PC for RTA 2007.

    To conclude, I believe automated reasoning has crucial contributions still to make to computer science and mathematics. I ask for your support for CADE trustee.

    Abstract of Recent Ph.D. Thesis in AR

    Author: Magnus Björk

    Title: A First-Order Extension of Stålmarck's Method

    Advisor: Mary Sheeran

    Date of defence: May 11, 2006

    Institution granting the degree: Department of Computer Science and Engineering, Chalmers University of Technology, Gothenburg, Sweden

    Abstract: Stålmarck's method is an algorithm that decides validity of formulae in propositional logic. It resembles many tableaux methods but uses a special branch-and-merge-rule, called the dilemma rule. The dilemma rule creates two branches, where a formula (called the dilemma formula) is assumed to be false in one branch and true in the other one. If neither of the branches turns out to be contradictory, then the branches are merged into one branch again, retaining the common consequences of the two branches.

    We present a first-order version of Stålmarck's method. When branches are merged in first-order logic, variables occurring in the respective branches are unified, to retain as much information as possible. We show that variables introduced in dilemma formulae must be treated rigidly in the branches of the dilemma where they were introduced, but that they are universal during and after the merge. Thus, the dilemma rule can be used to introduce lemmas with universal variables.

    We also present a proof procedure that searches for shallow dilemma proofs. It begins by searching for proofs not including the dilemma rule, then extends the search with non-nested dilemmas. After that, proofs with at most two simultaneously open dilemmas are found, then with three, and so on. The proof procedure does not substitute rigid variables destructively; instead it explores an instance of the current dilemma, after the branches have been merged. This is done to preserve as many generalized conclusions as possible, and to be able to find new dilemma formulae.

    We show that the calculus and proof procedure are sound and complete. We present encouraging benchmarks for the automated theorem prover Dilemma, which is based on the method.

    Author's correspondence address:
    E-mail: mab@cs.chalmers.se

    FMCAD 2006: Call for Participation

    The International Conference on Formal Methods in Computer-Aided Design will take place November 12-16, 2006, in San Jose, California (note: ICCAD also takes place in San Jose the previous week, Nov. 5-9). FMCAD 2006 is the sixth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. In addition to the technical program, FMCAD will offer a full day of tutorials:

    FMCAD will also include a panel on complementing simulation with formal methods and an affiliated workshop on pre- and postsilicon verification.

    The early registration deadline is October 22, 2006. For more information, see the Web site.

    Logic Summer School:
    The Australian National University

    The Logic Summer School at the Australian National University (ANU), to be held December 4-14, 2006, will comprise a blend of practical and theoretical short courses on aspects of pure and applied logic taught by international and national experts. The school provides a unique learning experience for all participants, backed up with state-of-the-art computational science facilities at the ANU.

    Program Topics

    The summer school is intended for (1) students from about the third year of undergraduate studies up to beginning Ph.D. level who are considering specializing in a logic-related field; (2) teachers who teach logic in computer science, mathematics, or philosophy; (3) IT professionals who use formal methods or who want to know more about logic-based technology; and (4) anyone who finds the idea of two weeks of wall-to-wall logic enticing!


    Professionals: $1,650 per person; discounts are available for multiple registrations from individual companies and institutions.

    Students in full-time education: $120 per person; scholarships are available and are assessed on a case-by-case basis. The Web site has more details.

    Registrations after Friday, 27 October 2006, are subject to a 20% surcharge. To register or for more information visit the Web site.

    Call for Papers

    The 18th International Conference on Rewriting Techniques and Applications (RTA'07) will take place in Paris, France, June 26-28, 2007. RTA-07 is organized as part of the Federated Conference on Rewriting, Deduction, and Programming (RDP'07), which comprises, in addition to RTA'07, the conference on Typed Lambda Calculi and Applications (TLCA'07) and eight workshops (HOR, PATE, RULE, SecReT, UNIF, WFLP, WRS, and WST).

    RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include

    Best Paper Award: An award is given to the best paper or papers as decided by the program committee.

    Submissions: Submission categories include regular research papers and system descriptions. Problem sets and submissions describing interesting applications of rewriting techniques are also welcome. The page limit for submissions is 15 pages in Springer LNCS style (10 pages for system descriptions). The submission Web page will be made available beginning of December. As usual, the proceedings of RTA'07 will be published in the Springer LNCS series. The deadline for electronic submission of title and abstract is Jan. 26, 2007; the deadline for electronic submission of papers is Jan. 31, 2007.

    Please consult the RTA'07 conference Web page for further information.

    CiE 2007

    The Third Conference CiE 2007, organized by CiE (Computability in Europe) will take place at the University of Siena, June 18-23 2007. CiE is a European network of mathematicians, logicians, computer scientists, philosophers, theoretical physicists and others interested in new developments in computability and in their underlying significance for the real world. CiE 2007 will address various aspects of the ways computability and theoretical computer science enable scientists and philosophers to deal with mathematical and real-world issues, ranging through problems related to logic, mathematics, physical processes, computation, and learning theory. At the same time it will focus on different ways in which computability emerges from the real world, and how this affects our way of thinking about everyday computational issues. Topics include artificial intelligence, formal methods, and uncertain reasoning.

    CiE 2007 will be colocated with the annual CCA (Computability and Complexity in Analysis) Conference June 16-18, 2007.

    Papers (max. 10 pages) are due Jan. 12, 2007. The conference proceedings will be published by LNCS, Springer Verlag. There will also be journal special issues, collecting invited contributions related to the conference. For further information, see the Web page.

    LICS 2007

    The 22nd annual IEEE Symposium on Logic in Computer Science will take place on July 10-14, 2007, in Wroclaw, Poland, colocated with ICALP 2007 and Logic Colloquium 2007. Topics include automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, formal methods, lambda and combinatory calculi, linear logic, logics in artificial intelligence, modal and temporal logics, reasoning about security, rewriting, and verification. Abstracts are due Jan. 15, 2007, with full papers due Jan. 22, 2007. For details, see the Web site.

    LICS Workshops

    Workshops are planned for July 8, 9 and July 15 (possibly the afternoon of 14th).

    LICS workshops have traditionally been an important and exciting part of the program. They introduce either newest research in traditional areas of the LICS community, recent interdisciplinary and applied areas of general theory, or emerging directions that already have some substantial overlap with LICS community interests. Researchers and practitioners are invited to submit proposals for workshops on topics relating logic - broadly construed - tocomputer science or related fields. Typically, LICS workshops feature a mix of invited speakers and contributed presentations. LICS workshops do not produce formal proceedings. However, in the past there have been special issues of journals based in part on certain LICS workshops.

    Proposals should include the following:

    Proposals are due Nov. 15, 2006, and should be submitted electronically to Philip Scott, Workshops Chair, LICS 2007, phil@site.uottawa.ca.


    The 14th Workshop on Logic, Language, Information and Computation will take place in Rio de Janeiro, Brazil, July 2-5, 2007.

    WoLLIC is an annual international forum on interdisciplinary research involving formal logic, computing and programming theory, and natural language and reasoning.

    Contributions (10 pages) 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; and foundational aspects of information organization, search, flow, sharing, and protection.

    Papers must be submitted electronically on the Web. A title and single-paragraph abstract should be submitted by February 23, 2007, with the full paper due March 2, 2007.

    Proceedings, including both invited and contributed papers, will be published in advance of the meeting.

    ASL sponsorship of WoLLIC'2007 will permit ASL student members to apply for a modest travel grant (deadline: April 1, 2007). See www.aslonline.org/studenttravelawards.html for details.

    TABLEAUX 2007

    TABLEAUX 2007 - Automated Reasoning with Analytic Tableaux and Related Methods - will take place 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 all aspects--theoretical foundations, implementation techniques, systems development and applications--of the mechanization of reasoning with tableaux and related methods. One or more tutorials will be part of the conference program.

    For further information, see the Web site.

    Special Issues


    The Journal on Satisfiability, Boolean Modeling and Computation will publish a special issue on satisfiability modulo theories.

    SMT is the problem of deciding the satisfiability of first-order formulas with respect to some decidable background theory (e.g., linear arithmetic, the theory of arrays, the theory of bit-vectors). SMT techniques are gaining increasing relevance in many application domains, including formal verification of hardware and software, compiler optimization, planning and scheduling. SMT is strongly related to SAT, as most SMT tools are built on top of or interface with efficient SAT solvers.

    Topics of interest for this special issue include novel general SMT techniques, novel SMT techniques for theories of interest, SMT for combined theories, novel implementation techniques for SMT, and applications of SMT. Submissions should be written in LaTeX and formatted according to JSAT's author guidelines, and should not exceed 20 pages. The deadline for paper submission (provisional) is November 25, 2006.

    The guest editors are Byron Cook (Microsoft Research - bycook@microsoft.com) and Roberto Sebastiani (DIT, Università di Trento - rseba@dit.unitn.it).

    For further information visit the Web page, or send an email to one of the guest editors.

    Computer Security: Foundations and Automated Reasoning

    In connection with the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), a satellite event of LICS'06 as part of FLoC 2006, a special issue of Information and Computation will be devoted to original papers on foundations and formal methods in computer security. Contributions are welcomed on the following topics and related ones:

    Authors should submit an abstract by Nov. 5, 2006. Full papers should be submitted electronically by Nov. 12, 2006, in portable document format (pdf) or postscript (ps), by sending an email with subject ``I&C submission'' to the address fcs-arspa06@lists.inf.ethz.ch with the file of the paper as an attachment.

    The guest editors are Pierpaolo Degano (Università di Pisa, Italy), Ralf Kuesters (ETH Zurich, Switzerland), Luca Vigano (ETH Zurich, Switzerland), and Steve Zdancewic (University of Pennsylvania, USA).

    For further information, see the Web site.

    Gail Pieper pieper@mcs.anl.gov
    October 2006