NEWSLETTER No. 77, September 2007

From the AAR President
Announcement of CADE Elections
Proposals for Sites for CADE-22 in 2009 Solicited
Call for Participation

  • Diagram 2008
  • TAP 2008
  • Open Positions
    Thesis Abstracts

    From the AAR President, Larry Wos... I am delighted by the number of people interested in becoming CADE trustees. I find their statements most impressive, with their recurring themes of exploring new ideas, encouraging young researchers, seeking new funding, investigating novel applications, and sponsoring awards.

    Would it not be marvelous to see the same excitement filling our subsequent issues of this newsletter as well as the Journal of Automated Reasoning! Program verification is mentioned as a challenging area: have you had any successes? I rely on others for implementations: have you implemented any new techniques that will give me more power, for example, to attack my favorite topic in finding shorter proofs? I look forward to hearing from you soon!

    Announcement of CADE Elections
    Wolfgang Ahrendt
    (Secretary of AAR and CADE)

    An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:

    Wolfgang Ahrendt (Secretary, appointed 5/2007)
    Alessandro Armando (IJCAR 2008 Program Co-chair)
    Franz Baader (President, CADE-19 Program Chair, elected 10/2003, reelected 10/2006)
    David Basin (IJCAR 2004 Program Co-chair, elected 10/2004)
    Peter Baumgartner (elected 10/2003, reelected 10/2006)
    Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004)
    Rajeev Goré (elected 10/2004)
    Reiner Haehnle (Vice President, elected 10/2005)
    Neil Murray (Treasurer)
    Frank Pfenning (CADE-21 Program Chair)
    Geoff Sutcliffe (elected 10/2004)
    Aaron Stump (elected 10/2006)
    Cesare Tinelli (elected 10/2005)

    The terms of David Basin, Maria Paola Bonacina, Rajeev Goré, and Geoff Sutcliffe are expiring. The position of Frank Pfenning is taken by Alessandro Armando as IJCAR 2008 program co-chair. Thus, there are four positions to fill.

    The following candidates (listed in alphabetical order) were nominated and their statements are below:

    Christoph Benzmueller nominated by Geoff Sutcliffe and Larry Paulson
    Maria Paola Bonacina Bonacina nominated by Reiner Haehnle and Uli Furbach Furbach
    br afelty Amy Felty Felty Felty nominated by Dale Miller and Brigitte Pientka
    Robert Nieuwenhuis nominated by Andrei Voronkov and Ashish Tiwari
    Brigitte Pientka Pientka nominated by Aaron Stump and Maria Paola Bonacina Bonacina
    br vxs Volker Sorge Sorge Sorge nominated by Alan Bundy and Simon Colton Colton
    Geoff Sutcliffe Sutcliffe Geoff nominated by Wolfgang Ahrendt and Koen Claessen Koen
    Koen voronkov Andrei Voronkov Andrei Voronkov nominated by Konstantin Verchinine and David Toman David


    Toman Statement by Christoph Benzm├╝ller Benzm├


    Automated deduction is a prestigious subfield of AI and there are numerous examples of mutual fertilization between the automated deduction area and other subfields of AI. Over the past decades automated deduction has become a mature discipline, and our systems have considerably gained in strength. Further impetus is possible by tightening links, for example, by a stronger exploitation of techniques from other AI areas and a tighter integration of our theorem provers with computer algebra techniques and decision procedures. Moreover, we need to explore novel applications, adapt our systems to their specific needs and provide better user interfaces for expert as well as nonexpert users. My own research in the past decade has been driven by such a wide range of interests and activities. Among others these include

    UL However, the main focus of my research has always been on the the theory and automation of classical higher-order logic. In my Ph.D. Ph thesis at Saarland University I have studied extensionality in in higher-order logic and implemented the higher-order resolution resolution prover LEO. In a project at Cambridge I am currently developing developing the successor LEO-II. LEO-II has a strong focus on tight and and fruitful cooperation with first-order provers such as E, Spass, Spass or Vampire in order to solve problems encoded in Church's Church simple type theory. An important next move for improving the the state of the art in automated higher-order theorem proving will will be to set up a higher-order TPTP infrastructure and to initiate initiate a higher-order CASC. In a collaboration with Geoff Sutcliffe Sutcliffe and others we have made a start in this direction, and a first first higher-order CASC happening is planned for next year's IJCAR. IJCAR

    Statement by Maria Paola Bonacina

    Being asked to write a statement for re-election as CADE trustee, I thought I would share a few thoughts about our field, referring to my web page for accomplishments in research, teaching, and service.

    We live at a time when it is widely acknowledged that computer technology is everywhere. On the other hand, the intellectual implications of the computing revolution are still not fully understood. Nevertheless, there is a growing awareness of how deeply computer science is changing the entire scientific enterprise, enterpriseincluding the humanities (e.g., Computer Science: Reflections on the Field, Reflections from the Field, Oct. 2004,; Towards 2020 Science, Mar. 2006,; Jeannette M. Wing, Computational Thinking, CACM 49(3):33-35, Mar. 2006, The scientific paradigm of mathematical theories and physical experiments is increasingly intertwined with the computational paradigm of models, procedures, languages to express them, and computer experiments, and mathematics itself is becoming computational.

    Then I keep asking myself: what is the role of automated reasoning in this exciting and challenging landscape? I think that if computer science becomes the "queen and servant" of all sciences, on a par with mathematics, automated reasoning should become the "queen and servant" of all fields of computer science. Automated reasoning should be for computer science the leap forward that quantum computing promises to be for electronics. A scientific endeavor alternates in its history phases of inward-looking, specialistic growth, with phases of open, universalistic development. Automated reasoning has been through a fruitful phase of the first kind and is ready to open up and reassert itself at the center of computer science, in the origin's spirit (to the question "Can machines think?" Alan Turing answered Yes, because the computing of a Turing machine is a kind of thinking). Our mission is to inject reasoning into all computer applications that are sufficiently complex to warrant it, without forgetting that a highest challenge of automated reasoning is reasoning about software and therefore about computing itself. To this end, we need a variety of engines, to be hidden inside applications, to make them more powerful and more beautiful, or to be integrated into reasoning environments that are easy, comfortable and pleasant to play with. Our field is young and full of marvelous challenges: it is with this mixture of reflection and excitement that I am ready to serve again the community as CADE trustee.

    Statement by Amy Felty

    It is an exciting time to be working in automated reasoning. Techniques and tools are maturing, and the number of applications of of the research and technology in this area is growing rapidly. There is a lot of diversity in our field, which helps make for interesting and fruitful conferences, both CADE and IJCAR. The IJCAR initiative has been quite successful, and I strongly support its continuation. I also strongly support CADE's role in supporting student participation, particularly through the Bledsoe Travel Award. Another strong point of CADE/IJCAR is the associated workshops, which provide the opportunity to bring people together to discuss and learn about specialized areas.

    I have participated in CADE at many levels for many years. My first paper appeared in 1988 and my most recent in 2005. I have also published in associated workshops including this year's LFMTP (Logical Frameworks and Metalanguages: Theory and Practice). In 1996, I was the Conference Chair of CADE when it participated in the first FLoC. I believe that FLoC is an excellent way to bring together even more people in related but diverse areas, and I fully support CADE/IJCAR's participation in future FLoC conferences. During the past three years (until May 2007), I have served as Secretary of CADE and Secretary-Treasurer of AAR (Association for Automated Reasoning), during a time of growth for AAR membership. I would like to continue my work with CADE as a trustee and work toward even more visibility and growth.

    Statement by Robert Nieuwenhuis

    Some conferences focus on a particular class of techniques and any applications of these, e.g., the conference on Rewriting Techniques and Applications (RTA), and other conferences focus on a particular kind of applications, using any kind of techniques, e.g., the conference on Computer-Aided Verification (CAV). CADE, the major forum for discussing all aspects of automated reasoning research, falls under both categories: it includes typical techniques, such as resolution, decision procedures, constraints, SAT, paramodulation, or tableaux, as well as typical applications, such as hardware and software development and verification, databases, mathematical reasoning or linguistics, to name just a few.

    Based on my experience as a PC-chair and PC-member of this and other conferences, I believe that it is crucial but not at all easy for a conference like CADE to maintain this leading role in both aspects, as a prestigious, broad, interesting, and attractive event, well known also in the large variety of potential application communities.

    Therefore, as a CADE trustee the viewpoint I would bring into discussion and defend is: (i) maintain equally high scientific standards when assessing the applicability and the theoretical quality of submitted work, and (ii) always have one single joint conference (inside FLoC or not) integrating at least CADE, Tableaux and FTP, that is always clearly visible under the same name (I would slightly prefer CADE over IJCAR), combined only with informal satellite workshops for discussing ongoing work.

    Statement by Brigitte Pientka

    In my view, CADE is the major venue for all aspects of automated reasoning research, and I regard it as the driving force to promote our field. While we should continue our emphasis on theoretical work and system building, I believe we should also reach out and welcome applications of our work in areas such as computer algebra, constraint solving, knowledge representation, mechanization of programming languages, and reasoning about programs. To foster synergy with other related areas, I would like to initiate discussions about collocating CADE with conferences on related areas. Joint events such as IJCAR and collocating with FLOC are also important ways to promote the visibility of our area and demonstrate the impact of our results to the general computer science community at large.

    My own research interest is in the theory and practice of logical frameworks. This includes: designing and investigating type theories and logics, building efficient verification and programming tools, and demonstrating their effectiveness using realistic applications. Since 2001, I have regularly published at CADE/IJCAR, ICLP, and, most recently, TPHOLs. In 2003, I received the best paper award at ICLP'03 for my work on higher-order term indexing, and I was invited to give a tutorial at ICLP'06 about my work.

    Over the past few years, I have been actively involved in promoting our field, and I recently proposed to organize CADE in Montreal in 2009. Over the previous years I was publicity chair for CADE 2005, PC member (PPDP'04, MFPS'05, ICLP'06, LPAR'07), organizer (2006, 2007) and program chair (2006) of the "Workshop for Logical Frameworks and Meta-theory: Theory and Practice," and area editor (theorem proving) for the Association of Logic Programming Newsletter (since 2005). As a CADE trustee, I intend to continue working toward ensuring that automated reasoning receives the attention it deserves.

    Volker Sorge

    My main research area is the application of automated reasoning in pure mathematics, in particular in algebraic domains. I have worked extensively on the integration of automated reasoning with other computational and AI methods, such as computer algebra and machine learning. I have organized several workshops at CADE, and regularly publish in CADE, IJCAR, and the Journal of Automated Reasoning. In my role as a Calculemus trustee, I was one of the people responsible for bringing Calculemus into IJCAR 2004. I am therefore very happy that Alan Bundy has nominated me as a CADE trustee.

    I believe that CADE is the leading and most influential automated reasoning conference today and that it is particularly pathbreaking in terms of the theoretical results presented. However, in my opinion, the key word "Automated" is often underrepresented in CADE, and I am particularly concerned that there are relatively few papers on implementations and applications at CADE. I strongly believe that CADE has an obligation to preserve the knowledge of advances in implementation techniques and applicability as it is otherwise at risk of being lost. I believe, therefore, that the most critical challenge to the community is to address this current need without damaging CADE's leading position in theory of automated reasoning. I therefore particularly support the IJCAR initiative as it not only exposes the CADE community to techniques outside the core field but also has a broader remit for applications and implementations.

    Statement by Geoff Sutcliffe

    I believe that the advancement and application of automated reasoning depends on recognizing and supporting the synergetic interaction of theoretical progress, high performance implementation (techniques), and application requirements. I strongly support research and development that leads to effective implemented systems. I expect CADE to remain the major forum for the presentation of new research in all aspects of automated deduction. As such CADE must reflect the depth, breadth, and interaction of all aspects of automated reasoning, to allow a broad automated reasoning community to use CADE as the preferred conference for the presentation of research results. I support CADE's efforts to provide financial assistance that enables young and poor researchers to attend the conference. I endorse CADE's leading role in IJCAR and continued participation in FLoC. I have recently taken on responsibility for publicity for CADE as an organization -- I already am the owner of the,, and domains, which are now the entry points to the respective web pages.

    I started my academic career at Edith Cowan University in 1986, taught at James Cook University from 1992 to 2001, and am now an associate professor at the University of Miami. I am probably best known in the automated reasoning community for the TPTP Problem Library, the CADE ATP System Competitions (CASC), and the "Empirically Successful" workshop series. Additionally, my "ARTists" research group is active in several aspects of automated reasoning. I have been attending CADE since CADE-10 in 1990 and have hosted CADE twice -- in Australia in 1997 and in Miami in 2003. I have been on the CADE program committee five times.

    Statement by Andrei Voronkov

    I contributed to research in automated deduction on many levels: by publishing 15 papers at CADE and IJCAR, implementing the theorem prover Vampire, editing the Handbook of Automated Reasoning, organizing many events in the area (LPAR, Dagstuhl Deduction workshops, Workshops on Implementation of Logic, other conferences and workshops), representing IJCAR on the FLoC steering committee, being vice president of CADE Inc. and CADE program chair, and working on applications in industry, including Intel and Microsoft. I attended every CADE/IJCAR since 1992.

    There is no doubt that CADE (as constituent of IJCAR, part of FLoC, or by itself) has been and will continue to be the major conference in automated reasoning. In the past some people regarded CADE as either very theoretical or very narrow but in the last years the scope of CADE has changed to the better in every respect.

    I have always thought that CADE should attract more papers in the newly developing areas and applications. To this end, in 2002 I nearly doubled the size of the CADE program committee and invited many people from other areas to it. In the same spirit, in 2003 when involved in organizing regular Dagstuhl Deduction workshops, I proposed to rename them in "Deduction and ..." and invited people from other areas.

    Now CADE attracts papers on a wide spectrum of topics. Yet I believe it should try to receive more high-quality papers from noncore areas. Indeed, best papers in applications of deduction in verification, constraints, semantic Web, SAT, and program analysis rarely appear at CADE.

    We should also try to attract young researchers to the area. To this end, we should start organizing (at least one) annual summer/winter school in automated reasoning involving also lecturers in areas where deduction is or can be used.

    There is another aspect in which the work of CADE Inc. should, in my opinion, be improved: financial. CADE has an excellent Woody Bledsoe award program for sponsoring students attending CADE. Nonetheless, I think it is not enough. We should more aggressively seek major funding in the area that would allow us to sponsor events and awards in the area and reduce CADE conference fees.

    Proposals for Sites for CADE-22 in 2009 Solicited

    We invite proposals for sites around the world to host the Conference on Automated Deduction (CADE) to be held in summer 2009 as a stand-alone conference. In some other years, CADE is held as part of FLoC and sometimes merges with other automated reasoning conferences into IJCAR.

    CADE's/IJCAR's recent location history is as follows:

    2000: CADE-17 in North America
    2001: IJCAR 2001 in Europe
    2002: CADE-18 as part of FLoC in Europe
    2003: CADE-19 in North America
    2004: IJCAR 2004 in Europe
    2005: CADE-20 in Europe
    2006: IJCAR 2006 as part of FLoC in North America
    2007: CADE-21 in Europe

    CADE's/IJCAR's near location future will be as follows:

    2008: IJCAR 2008 in Australia
    2009: (this call)
    2010: IJCAR 2010 as part of FLoC in Europe

    The deadline for proposals is November 16, 2007. We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.

    Proposals should address the following points that also represent criteria for evaluation:

    Perspective organizers are encouraged to get in touch with the CADE secretary and president (see contact information below) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.

    Franz Baader, CADE President (
    Wolfgang Ahrendt, CADE Secretary (

    Special Issue of Studia Logica

    Further to the highly successful Studia Logica International Conference Trends in Logic V, held in Guangzhou, China, during July 6-9, 2007, we cordially invite people to submit a paper for a special issue of Studia Logica devoted to many-valued logic and cognition. We especially invite contributions on the following.

    TPTP Version 3.3.0 Released
    Geoff Sutcliffe
    Department of Computer Science, University of Miami

    The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with the following.

    The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.

    TPTP v3.3.0 is now available on the Web. The TPTP-v3.3.0.tar.gz file contains the library, including utilities and basic documentation. Full documentation is online.

    The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user and be kept informed of such developments, please email Geoff Sutcliffe.

    What's New in TPTP v3.3.0

    Call for Participation

    The 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2007) will take place in Austin, Texas, on November 11-14, 2007. Early registration will open mid-September; refer to the Web for more information and updates.

    FMCAD 2007 is the seventh in a series of conferences on the theory and application of formal methods in hardware and system design and verification. In 2005, the bi-annual FMCAD and sister conference CHARME decided to merge to form an annual conference with a unified community. The resulting unified FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for formally reasoning about computing systems, as well as open challenges therein. FMCAD2007 will include a full day of tutorials and will be collocated with the ACL2 Workshop.

    Call for Papers

    Diagrams 2008

    The 5th International Conference on the Theory and Application of Diagrams (Diagrams 2008) will take place in Germany on September 19-21, 2008.

    Diagrams is the only conference that provides a united forum for all areas that are concerned with the study of diagrams: for example, architecture, artificial intelligence, cartography, cognitive science, computer science, education, graphic design, history of science, human-computer interaction, linguistics, logic, mathematics, philosophy, psychology, and software modeling.

    Diagrams will run in conjunction with the IEEE Symposium on Visual Languages and Human-Centric Computing and the ACM Symposium on Software Visualization as part of Visual Week.

    Topics of particular interest to AAR members include the following:

    Diagrams 2008 will consist of sessions including presentations of refereed papers, posters and tutorial sessions. We invite submissions of long research papers (15 pages), short research papers (7 pages) posters (3 pages), and tutorial proposals (1 page; see the conference web page for full fulldetails) that focus on any aspect of diagrams research. Long papers should present original research results. Short papers and posters should present original research contributions, position, or problem statements; summarize software to support the use of diagrams; or integrate results published elsewhere that are of interest to the Diagrams community. The proceedings will be published by Springer in their Lecture Notes in Computer Science series. series

    Important Dates:

    Abstract submission: March 20, 2008
    Paper and tutorial submission: April 1, 2008
    Poster submission: April 11, 2008

    For further information, see the Web site.

    TAP 2008

    The second international conference on Tests and Proofs (TAP) will be held on April 9-11, 2008, in Prato (near Florence), Italy. TAP is devoted to the convergence of proofs and tests. It combines ideas from both sides for the advancement of software quality.

    To prove the correctness of a program is to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a program is to run it with the expectation of discovering bugs. The two techniques seem contradictory: if you have proved your program, it's fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on any hope to prove its correctness. Accordingly, proofs and tests have, since the onset of software engineering research, been pursued by distinct communities using rather different techniques and tools. And yet the development of both approaches leads to the discovery of common issues and to the realization that each may need the other. The emergence of model checking has been one of the first signs that contradiction may yield to complementarity, but in the past few years an increasing number of research efforts have encountered the need for combining proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer.

    How does deduction help testing? How does testing help deduction? How can the combination of testing and deduction increase the reach of both? These and topics such as the following are welcome:


    The abstracts are due November 2, 2007; the papers are due November 9, 2007. Submissions should describe previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. Papers must be formatted following the Springer LNCS guidelines and be at most 15 pages long. Submission of papers is via The proceedings are planned to be published within Springer's LNCS series and will be available at the conference.

    For further information, please see the Web site, or send email to

    Open Positions

    The newly formed group Laboratory for Automated Reasoning and Analysis has open Ph.D. positions in the area of automated reasoning and verification. To apply, please contact Viktor Kuncak.

    Mailing Address:
    Swiss Federal Institute of Technology (EPFL)
    School of Computer & Communications Sciences
    Building INR318
    Station 14
    CH-1015 Lausanne

    Thesis Abstracts

    Title of Thesis: Modular Data Structure Verification
    Author: Viktor Kuncak
    Institution: Massachusetts Institute of Technology
    Thesis Supervisor: Martin C. Rinard
    Current Web page:
    Abstract: This dissertation describes an approach for automatically verifying data structures, focusing on techniques for automatically proving formulas that arise in such verification. I have implemented this approach with my colleagues in a verification system called Jahob. Jahob verifies properties of Java programs with dynamically allocated data structures.

    Developers write Jahob specifications in classical higher-order logic (HOL); Jahob reduces the verification problem to deciding the validity of HOL formulas. I present a new method for proving HOL formulas by combining automated reasoning techniques. My method consists of (1) splitting formulas into individual HOL conjuncts, (2) soundly approximating each HOL conjunct with a formula in a more tractable fragment, and (3) proving the resulting approximation using a decision procedure or a theorem prover. I present three concrete logics; for each logic I show how to use it to approximate HOL formulas, and how to decide the validity of formulas in this logic.

    First, I present an approximation of HOL based on a translation to first-order logic, which enables the use of existing resolution-based theorem provers. Second, I present an approximation of HOL based on field constraint analysis, a new technique that enables decision procedures for special classes of graphs (such as monadic second-order logic over trees) to be applied to arbitrary graphs.

    Third, I present an approximation using Boolean Algebra with Presburger Arithmetic (BAPA), a logic that combines reasoning about sets of elements with reasoning about cardinalities of sets. BAPA can express relationships between sizes of data structures and invariants that correlate data structure size with integer variables. I present the first implementation of a BAPA decision procedure, and establish the exact complexity bounds for BAPA and quantifier-free BAPA.

    Together, these techniques enabled Jahob to modularly and automatically verify data structure implementations based on singly and doubly-linked lists, trees with parent pointers, priority queues, and hash tables. In particular, Jahob was able to prove that data structure implementations satisfy their specifications, maintain key data structure invariants expressed in a rich logical notation, and never produce run-time errors such as null dereferences or out of bounds accesses.

    Title of Thesis: Combined Decision Procedures for Constraint Satisfiability
    Author: Enrica Nicolini
    Institution: Universita' degli Studi di Milano (Italy)
    Date of Defense: Jan. 4, 2007
    Current Web page: A pdf file is available from the Web.
    Abstract: This thesis is devoted to the study of the decidability of fragments of different logical languages and the transfer of the decidability to their combination. Our work first shows that the universal fragment of the theory of arrays with dimension is decidable, and then it concentrates on combination problems. If we consider the union of two first-order theories over disjoint signatures, we prove that the constraint satisfiability problem (c.s.p.) for the combination of two theories whose c.s.p. is decidable is in general undecidable, but nevertheless it is possible to weaken the standard additional hypothesis of stably infiniteness in order to regain the decidability.

    As far as the combination of two theories over non-disjoint signature is concerned, we introduce the notion of noetherianity that, together with the already-known requirement of 'T_0 compatibility,' is sufficient for transferring the decidability of the c.s.p. We also generalize the Nelson-Oppen combination schema by plugging it into a higher-order framework. The main advantage of this choice is the opportunity to consider in a uniform way a large variety of logical fragments, deriving thus new decidability results. As an example, we analyze monodic modal/temporal fragments as combinations of extensional first-order fragments and standard translations of one variable modal/temporal fragments, finally obtaining rather general decidability transfer results.

    Gail Pieper 2007-09-06