NEWSLETTER
No. 73, December 2006

From the AAR President

Results of the CADE Elections 2006

CADE-21

Proposals Solicited for Sites for IJCAR 2008

Call for Papers

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

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.

Papers are sought in the following areas:

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.

Workshop proposals should include the following:

- Name and a brief description of the workshop, specifying its motivation, goal and topics
- History of the workshop (if any), including Web pointers and prior collocation information
- Estimated number of workshop submissions and participants
- Proposed format and expected duration (1 or 2 days)
- Planned submission and selection procedure (including a tentative schedule)
- Workshop chair(s) and organizing committee

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:

- National, regional, and local AR community support:
- IJCAR Conference Chair and host institution,
- IJCAR Local Arrangements Committee,
- availability of (and reward for) student-volunteers.

- National, regional, and local government and industry support, both organizational and financial
- Accessibility (i.e., transportation), attractiveness, and desirability of proposed site.
- 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).
- 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.
- 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.
- 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.
- 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

baader@tcs.inf.tu-dresden.de

baader@tcs.inf.tu-dresden.de

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

For further information visit the Web site.

- New decision procedures and new theories of interest
- Combination of decision procedures
- Novel implementation techniques
- Benchmarks and evaluation methodologies
- Applications and case studies
- Theoretical results

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.

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

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.

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

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:

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.

- 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

pieper@mcs.anl.gov

December 2006