NEWSLETTER No. 73, December 2006

From the AAR President
Results of the CADE Elections 2006

  • CADE-21 Papers
  • CADE-21 Workshop Proposals

  • Proposals Solicited for Sites for IJCAR 2008
    Call for Papers
  • FroCoS 2007
  • SMT Workshop

  • Wanted: An Automated "Learning Strategy" for Automated Reasoning
    Special Issue of JSAT: Call for Papers
    Bedwyr: A Proof Search Approach to Model Checking

    From the AAR President, Larry Wos...

    Are you looking for a great Christmas present to yourself or someone who enjoys logical reasoning? How about a subscription to the Journal of Automated Reasoning? For AAR members it is a real bargain--still only $93 for eight issues. That's just about a quarter a day. You couldn't even buy an espresso for that (if you are one of those who--for some reason I cannot fathom--claim to like espresso).

    The Journal was established over two decades ago to provide a forum for those interested in automated reasoning and logic. AAR and the AAR Newsletter were established shortly thereafter. The newsletter was intended to give people information about activities in the field and provide an informal mechanism for exchanging ideas and announcing new contributions. In that vein, I call your attention to two items: (1) the article in this issue about the Bedwyr project, which is seeking applications from interested readers, and (2) my article on a new "learning" strategy, which I hope an AAR member will implement in OTTER or in another reasoning system.

    Results of the CADE Trustee Elections 2006
    Amy Felty
    (Secretary of AAR and CADE)

    An election was held from October 13 through November 3 to fill three positions on the board of trustees of CADE Inc. Franz Baader, Peter Baumgartner, Chris Benzmueller, and Aaron Stump were nominated for these positions. (See AAR Newsletter No. 72, October 2006.)

    Ballots were sent by electronic mail to all members of AAR on October 13, for a total of 699 ballots (as compared to 631 ballots in 2005, 630 in 2004, and 587 in 2003). Of these, 112 were returned with a vote, representing a participation level of 16.0% (as compared to 18.1% in 2005 and 19.8% in 2003 and 2004). The majority is 50% of the votes plus 1, hence 57.

    The following table reports the initial distribution of preferences among the candidates:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    F. Baader 53 29 16 14 112
    P. Baumgartner 27 41 28 16 112
    C. Benzmueller 18 10 27 57 112
    A. Stump 14 31 36 31 112

    No candidate reaches a majority right away. The redistribution of the votes of A. Stump (the candidate with the lowest number of first preference votes) yields the following new distribution:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    F. Baader 61 30 20 1 112
    P. Baumgartner 32 57 23 0 112
    C. Benzmueller 19 24 64 5 112

    F. Baader has a majority of votes and is thus elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    P. Baumgartner 56 35 21 0 112
    C. Benzmueller 24 26 61 1 112
    A. Stump 32 46 33 1 112

    Again, no candidate reaches a majority, and by redistributing the votes of C. Benzmueller, one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    P. Baumgartner 70 42 0 0 112
    A. Stump 42 65 4 1 112

    Thus, P. Baumgartner is elected to the board of trustees. The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    C. Benzmueller 39 72 1 0 112
    A. Stump 68 43 1 0 112

    Thus, A. Stump is elected to the board of trustees.

    After this election, the following people are serving on the board of trustees of CADE Inc.:

    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)
    Amy Felty (Secretary, appointed 5/2004)
    Rajeev Goré (elected 10/2004)
    Reiner Hähnle (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)

    On behalf of the AAR and CADE Inc., I thank Michael Kohlhase for his service as trustee during the past six years, Uli Furbach for his service as trustee during the past year, all candidates for running in the election, and all the members who voted; and I offer congratulations to Franz Baader, Peter Baumgartner, and Aaron Stump on being elected.


    The 21st International Conference on Automated Deduction (CADE-21) will be held at International University Bremen, Germany, July 17-20, 2007, with workshops on July 15-16.

    CADE is the major forum for the presentation of research in all aspects of automated deduction.

    CADE-21 Papers

    Papers are sought in the following areas:

  • Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory.
  • Methods of interest include resolution, tableaux, term rewriting, induction, unification, constraint solving, SAT solving, decision procedures, saturation, model generation, model checking, natural deduction, sequent calculi, proof planning, proof presentation, proof checking, and explanation.
  • Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI.
  • Submission is electronic in PostScript or PDF format via the EasyChair system. Submitted papers must conform to the Springer LNCS style, preferrably using LaTeX2e and the Springer llncs class files. Submissions can be full papers, for work on foundations, applications, or implementation techniques (15 pages), as well as system descriptions (5 pages), for describing publicly available systems. The proceedings will be published in the Springer LNCS series. For further information and submission instructions, see the Web page.

    The deadline for submission of title and abstract is February 16, 2007. Full papers must be submitted by February 23, 2007.

    CADE-21 Workshop Proposals

    The main CADE conference will be preceded on July 15-16 by workshops. They will provide an environment where participants will have the opportunity to discuss specific topics in an atmosphere that fosters the active exchange of ideas.

    Researchers are invited to submit workshop proposals for review. Proposals related to automated deduction topics (see the Web site above) as well as proposals at the boundary between automated deduction and other research fields are welcome. We encourage proposals that build on previous events as well as proposals that are new.

    Workshop participants will not be required to register for CADE-21; instead, there will be independent workshop registration fees.

    Workshop organizers may choose to have their proceedings/notes printed and distributed by the organizers of CADE-21. All organizers are expected to provide an on-line version of their proceedings/notes, which will be made accessible via the official CADE-21 conference Web site.

    Workshop proposals should include the following:

    The proposal submission deadline is Dec. 15, 2006. Proposals should be submitted electronically to Christoph Benzmueller, The University of Cambridge, CADE-21 Workshop Chair;

    The proposals will be reviewed and selected by the CADE-21 conference chair (Michael Kohlhase), the CADE-21 program chair (Frank Pfenning), and the CADE-21 workshop chair (Christoph Benzmueller).

    Proposals Solicited for Sites for IJCAR 2008

    We invite proposals for sites around the world to host the Fourth International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2008. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; and IJCAR 2006 as part of FLoC in Seattle, Washington.

    The fourth IJCAR will be a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), FroCoS (Workshop on Frontiers of Combining Systems), FTP (Workshop on First-order Theorem Proving), and possibly other meetings.

    The deadline for proposals is January 3, 2007. Proposals should be sent to the IJCAR Steering Committee Chair (see contact information below). We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date.

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

    1. National, regional, and local AR community support:
      • IJCAR Conference Chair and host institution,
      • IJCAR Local Arrangements Committee,
      • availability of (and reward for) student-volunteers.
    2. National, regional, and local government and industry support, both organizational and financial
    3. Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
    4. Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls).
    5. Conference and exhibit facilities for the anticipated number of registrants (typically up to 200), for example, number, capacity and audiovisual equipment of meeting rooms; a large plenary session room that can hold all the registrants; enough rooms for parallel sessions/workshops/tutorials; Internet connectivity and workstations for demos/competitions; catering services; and presence of professional staff.
    6. Residence accommodations and food services in a range of price categories and close to the conference facilities, for example, number and cost range of hotels, and availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer.
    7. Rough budget projections for the various budget categories, e.g., cost of renting/cleaning the meeting rooms, if applicable; cost of professional conference secretariat, if hired; and financial model for satellite workshops and/or collocated events.
    8. Balance with regard to the geographical distribution of previous IJCAR and its constituent meetings.

    Perspective organizers are encouraged to get in touch with the IJCAR Steering Committee Chair 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, IJCAR Steering Committee Chair

    Call for Papers

    FroCoS 2007

    FroCoS 2007, the International Symposion on Frontiers of Combining Systems, will take place in Liverpool, UK, September 10-12, 2007.

    Typical topics of interest include combinations of logics such as combined predicate, temporal, modal, or epistemic logics; combinations and modularity in ontologies; combination of decision procedures, of satisfiability procedures, and of constraint solving techniques; combinations and modularity in term rewriting; integration of equational and other theories into deductive systems; combination of deduction systems and computer algebra; logical aspects of combining and modularising programs and specifications. The submission deadline is April 30, 2007.

    FroCoS will be collocated with FTP (Workshop on First-order Theorem Proving).

    For further information visit the Web site.

    SMT Workshop '07

    The 5th International Workshop on Satisfiability Modulo Theories (SMT Workshop '07), previously called Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), will take place in Berlin, Germany, July 1-2, 2007; it will be affiliated with CAV '2007.

    Deciding the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be useful in verification, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each concrete theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit vectors) and combination methods that allow one to obtain more versatile SMT tools. These two ingredients together make SMT techniques well suited for use in larger automated reasoning and formal verification efforts.

    The aim of the SMT '07 workshop is to bring together researchers and users of SMT tools and techniques. Continuing with the PDPAR tradition, we especially encourage submission of papers focused on pragmatic aspects. Relevant topics include the following:

    There are two categories of submissions:

    The submission deadline is April 23, 2007.

    Papers in both categories will be peer-reviewed. Papers should not exceed 10 pages (Postscript or PDF) and should be written in LaTeX. submission guidelines are at the workshop Web page.

    Only informal proceedings will be distributed at the workshop. We are planning to publish a selected subset of the submitted papers as postproceedings in a special volume of the Electronic Notes in Theoretical Computer Science (ENTCS) unless the authors prefer not to.

    Program chairs are Sava Krstic (Intel Corporation) and Albert Oliveras (Tech. Univ. of Catalonia).

    Wanted: An Automated "Learning Strategy" for Automated Reasoning
    Larry Wos

    Automated reasoning programs continue to (in effect) ask for more strategy. This article offers a strategy somewhat in the spirit of "learning", with the hope that someone will choose to implement it and make it available to researchers.

    First, recall that the resonance strategy has the researcher rely on formulas or equations that guide a program's reasoning [1]. Each resonator is treated as an attractive template where all variables are considered as indistinguishable--that is, treated merely as a variable. Resonators are not assigned a truth value.

    The basic idea is to have a program augment its set of included resonators during the run--a kind of dynamic resonance strategy. To encode this strategy, one places (in the paradigm used by OTTER [2]) targets to be proved. If and when a target, say a lemma, is proved, the program pauses to consider the corresponding proof. The proof steps of the proof are added as resonators, each with an assigned value that is small, to give high priority to conclusions that match one of the new proof steps. In addition, the program examines all of its retained conclusions, changing their priority consistent with the new set of priorities dictated by the newly adjoined resonators. A quick analysis of the preceding shows why the strategy does, in some part, capture the spirit of learning.

    Immediately, one might wonder why this idea is attractive. Has it been tried? Not to my knowledge: However, in an iterative sense, it has proved quite powerful. Specifically, I have placed in list(passive) a number of lemmas to be proved. After some chosen CPU time, I have stopped the run, extracted the proofs of those lemmas proved, placed them as resonators in the now-larger set of resonators, and resumed. I have been able to get a number of proofs in this manner that eluded me before using it.

    Of course, the automated version I'd like to see implemented would work somewhat differently from the iterative approach I've used because, among other aspects, the order of retained information would be affected. Most important, the sought-after approach would not require user intervention. Indeed, the program would do selection and placement of the new resonators, allowing the researcher to enjoy a multicourse dinner or go shopping for the holidays!


    1. Wos, L., ``The Resonance Strategy,'' Computers and Mathematics with Applications, 29, no. 2, 133-178 (February 1995)

    2. McCune, W., ``Otter 3.3 Reference Manual,'' Tech. Memo ANL/MCS-TM-263, Argonne National Laboratory, Argonne, IL, 1994.

    Special Issue of JSAT: Call for Papers
    Miroslav Velev and Joao Marques-Silva
    Editors of the special issue of JSAT on CFV

    We invite researchers to submit a paper to the special issue of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT) on the topic of application of constraints to formal verification (CFV).

    The submission deadline is January 10, 2007.

    Topics of interest include the following:

    The submissions must be in the JSAT format as stated on the Web page. Submissions should be e-mailed to If possible, please confirm your intent to submit a paper.

    Bedwyr: A Proof Search Approach to Model Checking

    Bedwyr is a programming framework written in OCaml that facilitates natural and perspicuous presentations of rule oriented computations over syntactic expressions and that is capable of model checking based reasoning over such descriptions.

    Bedwyr is in spirit a generalization of logic programming. However, it embodies two important recent observations about proof search:

    1. It is possible to formalize both finite success and finite failure in a sequent calculus; proof search in such a proof system can capture both "may" and "must" behavior in operational semantics specifications.

    2. Higher-order abstract syntax can be supported at a logical level by using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions; these features allow reasoning directly on expressions containing bound variables.

    The distribution of Bedwyr includes illustrative applications to the finite pi-calculus (operational semantics, bisimulation, trace analyses and modal logics), the spi-calculus (operational semantics), value-passing CCS, the lambda-calculus, winning strategies for games, and various other model-checking problems. These examples should also show the ease with which a new rule based system and particular questions about its properties can be be programmed in Bedwyr. Because of this characteristic, we believe that the system can be of use to people interested in the broad area of reasoning about computer systems.

    The present distribution of Bedwyr has been developed by the following individuals: David Baelde and Dale Miller (INRIA and LIX/Ecole Polytechnique), Andrew Gacek and Gopalan Nadathur (University of Minneapolis), and Alwen Tiu (Australian National University and NICTA).

    In the spirit of an open source project, we welcome contributions in the form of example applications and also new features from others. Please see the Web page.

    Gail Pieper
    December 2006