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:

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:

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:

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

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

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.

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

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

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.

There are two categories of submissions:

• Original papers: contain original research (simultaneous submissions are not allowed) and sufficient detail to assess the merits and relevance of the submission. For papers reporting experimental results, authors are strongly encouraged to make their data available. Given the informal style of the workshop, work in progress will be welcome.

• Presentation-only papers: describe work recently published or submitted and will not be included in the proceedings. We see this as a way to provide additional access to important developments that SMT Workshop attendees may be unaware of.

The submission deadline is April 23, 2007.

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!

References

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.

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:

• application of constraint solvers to hardware verification;
• application of constraint solvers to software verification;
• dedicated solvers for formal verification problems;
• tuning SAT for formal verification and testing;
• challenging formal verification problems.

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