We end this year with the excellent news that our membership has again increased, following a trend since 1999. The current AAR membership is now 631. Those who know me will not be surprised, then, when I offer the following challenge: Let us increase our membership to the much more pleasing number of 660 by June 6, 2006.

In welcoming the two new CADE trustees, Reiner Hähnle and Cesare Tinelli, I offer another challenge as well: Let us use the AAR Newsletter as a forum for discussion of significant issues in automated reasoning and as a mechanism for presentation of open questions.

An election was held from October 14 through November 4 to fill two positions on the board of trustees of CADE Inc. Didier Galmiche, Reiner Hähnle, Aaron Stump, Cesare Tinelli, and Toby Walsh were nominated for these positions. (See AAR Newsletter No. 68, October 2005.)

Ballots were sent by electronic mail to all members of AAR on October 14, for a total of 631 ballots (similar to 630 ballots in 2004, and up from 587 in 2003, 566 in 2002, 548 in 2001, 445 in 2000 and 396 in 1999). Of these, 114 were returned with a vote, representing a participation level of 18.1% (down from 19.8% in 2003 and 2004, 26.3% in 2002, 22.5% in 2001, 24.5% in 2000, and 30% in 1999). The majority is 50% of the votes plus 1, hence 58.

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:

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

Again, no candidate reaches a majority. C. Tinelli and T. Walsh have the same number of first preference votes, but Tinelli is higher in the ranking because of receiving more second preference votes. The redistribution of the votes of T. Walsh yields the following new distribution:

Thus, R. Hähnle is elected to the board of trustees. (Since 57 votes does not suffice for the majority, the STV algorithm executes another round distributing the votes of C. Tinelli, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:

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

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

Thus, C. Tinelli is elected to the board of trustees. (As before, another round of the STV algorithm gives C. Tinelli a majority.)

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)
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 co-Program Chair)
Rajeev Gor'e (elected 10/2004)
Reiner Hähnle (elected 10/2005)
Michael Kohlhase (elected 10/2000, reelected 10/2003)
Neil Murray (Treasurer)
Geoff Sutcliffe (elected 10/2004)
Cesare Tinelli (elected 10/2005)

In addition, the proposed amendment of the CADE bylaws regarding the election of the CADE president (see AAR Newsletter No. 68, October 2005) did not pass because not enough AAR members voted.

On behalf of the AAR and CADE Inc., I thank Andrei Voronkov for his service as trustee during the past four years and his service as CADE Inc. vice president during the past year; Toby Walsh for his service as trustee during the past three years; and Robert Nieuwenhuis for his service as trustee during the past year. I thank all candidates for running in the election and all the members who voted. And I offer congratulations to Reiner Hähnle and Cesare Tinelli on being elected.

We invite proposals for sites around the world to host the Conference on Automated Deduction (CADE) to be held in summer 2007. Normally, CADE alternates between North America and Europe; however, CADE is sometimes held as part of FLoC and sometimes merges with other automated reasoning conferences as IJCAR, so the pattern may vary. CADE's recent history is as follows:

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

1. National, regional, and local AR community support, including CADE Conference Chair and host institution, CADE Local Arrangements Committee, and 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 150-300), 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, for example, 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 conferences.

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 (baader@tcs.inf.tu-dresden.de)

Amy Felty, CADE Secretary (afelty@site.uottawa.ca)

We are pleased to present the following abstract of a recent thesis in automated reasoning.

Author: Hristo Koshutanski

Title: Interactive Access Control for Autonomic Systems

Supervisor: Fabio Massacci

Date of Defense: March 25, 2005

Institution: University of Trento, Italy

Abstract: Autonomic communication and computing is the new paradigm for dynamic service integration over a network. An autonomic network crosses organizational and management boundaries and is provided by entities that see each other just as partners that need to collaborate with little known or even unknown parties. Policy-based network access and management already requires a paradigm shift in the access control mechanism: from identity-based access control to trust management and negotiation but even this is not enough for cross-organizational autonomic communication.

For many services no autonomic partner may guess a priori what will be sent by clients and clients may not know a priori what credentials are demanded for completing a service, which may require the orchestration of many different autonomic nodes.

To solve this problem we propose to use interactive access control: servers should be able to get back to clients asking for missing or excessing credentials, whereas the latter may decide to supply or decline requested credentials and so on until a final decision is taken.

This proposal is grounded in a formal model on policy-based access control. It identifies the automated reasoning services of deduction, abduction and consistency checking that characterize the problem. It proposes two access control algorithms for stateless and stateful autonomic services and show their completeness and correctness.

Then it introduces an interactive trust negotiation protocol that communicates and negotiates the missing credentials in a piecewise manner. The protocol can be run on a client and a server side so that they understand each other and automatically interoperate until a desired solution is reached or denied.

Finally, an implementation of the framework is presented.

Call for Papers

Automated Reasoning for Logic

• Investigations of axiomatizations of logics
• Proof search and guidance for reasoning about logics
• System descriptions specialized toward reasoning about logics
• Experimental results from automated reasoning about logics
• Challenge problems in logic for automated reasoning
• Encoding application problems as logic problems
• Applications of automated reasoning for logic

Nominations are invited for the Ackermann Award 2006 - the EACSL Outstanding Dissertation Award for Logic in Computer Science. The award will be presented to the recipient(s) at the annual conference of the EACSL (CSL'06). The first Ackermann Award was presented at CSL'05 to Mikolaj Bojanczyk, Konstantin Korovin, and Nathan Segerlind. Eligible for the 2006 Ackermann Award are Ph.D. dissertations that were accepted at a university or equivalent institution between January 1, 2004, and December 31, 2005, and that were in topics specified by the EACSL and LICS conferences. The award consists of a diploma, an invitation to present the thesis at the CSL conference, the publication of the abstract of the thesis and the laudation in the CSL proceedings, and travel support to attend the conference.

Description logics (DLs) are a successful family of logic-based knowledge representation formalisms, which can be used to represent the conceptual knowledge of an application domain in a structured and formally well-understood way. They are employed in various areas, such as natural language processing, configuration, and databases, but their most notable success so far is the adoption of the DL-based language OWL as ontology language for the Semantic Web.

The most important selling point for DL systems is that they provide their users with highly optimized reasoning procedures for expressive representation languages, which--despite their high worst-case complexity--behave quite well in practice. Most DL systems employ tableau-based reasoning procedures, but several promising alternative approaches to reasoning in DLs are currently investigated. The purpose of this special issue is to provide a snapshot of the current research on reasoning in DLs, which shows different approaches and ranges from theoretical to applied work.

Topics

This special issue is concerned with all aspects of reasoning in description logics. Topics of interest include the following:

• tableau-based reasoning procedures
• resolution-based reasoning procedures
• automata-based reasoning procedures
• translation-based reasoning procedures
• tractable reasoning in inexpressive DLs
• procedures for non-standard inference problems
• complexity of reasoning
• implementation and optimization techniques
• empirical evaluations of reasoning techniques
• application of reasoning in DLs

Submissions

This special issue seeks original high-quality contributions that have not been published in or submitted to any journal. Long versions of papers previously published at a conference are welcome, but the journal version must significantly extend the conference version (e.g., by new results; full proofs for theoretical papers; more thorough empirical evaluations for practical papers). The submissions will be refereed according to the usual standards of the Journal of Automated Reasoning.