AARNEWS - December 2005

ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 69, December 2005

From the AAR President
Results of the CADE Trustee Elections 2005
Proposals for Sites for CADE-21 in 2007 Solicited
Abstract of Recent Thesis
Call for Papers

  • IJCAR 2006
  • LARARL
  • RWCA 2006
  • TERMGRAPH 2006
  • PSI 2006
  • CAV 2006
  • ESSLLI 2006 Student Session
  • RTA'06
  • JELIA'06
  • Call for Nominations: Ackermann Award 2006
    Reasoning in Description Logics

    From the AAR President, Larry Wos...

    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.

    Results of the CADE Trustee Elections 2005

    Amy Felty
    (Secretary of AAR and CADE)
    E-mail: afelty@site.uottawa.ca

    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:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    D. Galmiche 18 11 16 8 61 114
    R. Hähnle 30 33 13 11 27 114
    A. Stump 9 19 15 18 53 114
    C. Tinelli 27 30 9 13 35 114
    T. Walsh 30 18 16 11 39 114

    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. 5th Pref. Total
    D. Galmiche 19 13 17 39 26 114
    R. Hähnle 32 35 18 15 14 114
    C. Tinelli 31 32 11 21 19 114
    T. Walsh 32 20 20 25 17 114

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

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    R. Hähnle 41 32 19 14 8 114
    C. Tinelli 36 33 22 14 9 114
    T. Walsh 36 25 25 18 10 114

    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:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    R. Hähnle 57 34 6 17 0 114
    C. Tinelli 50 40 8 15 1 114

    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:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    D. Galmiche 25 15 12 46 16 114
    A. Stump 13 26 22 39 14 114
    C. Tinelli 40 21 17 29 7 114
    T. Walsh 35 27 11 31 10 114

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

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    D. Galmiche 26 20 34 26 8 114
    C. Tinelli 45 28 20 16 5 114
    T. Walsh 40 29 20 23 2 114

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

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. 5th Pref. Total
    C. Tinelli 55 35 11 11 2 114
    T. Walsh 50 35 10 19 0 114

    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.

    Proposals for Sites for CADE-21 in 2007 Solicited

    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:

    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
    The deadline for proposals is January 31, 2006. In addition, 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:

    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)

    Abstract of Recent Thesis

    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

    IJCAR 2006

    The Third International Joint Conference on Automated Reasoning (IJCAR 2006) will take place on August 16--21, 2006, in Seattle, Washington. IJCAR 2006 is the fusion of several major conferences in automated reasoning: CADE, TABLEAUX, FTP, FroCoS, and TPHOLs. IJCAR 2006 will be part of FLoC'06, to be held in Seattle August 10-22, 2006.

    Research papers and descriptions of working automated deduction systems are solicited. Research papers (max. 15 pages) and system descriptions (max. 5 pages) must be original and not submitted for publication elsewhere. In the research paper category, submissions of theoretical, practical, and experimental nature are equally encouraged. Authors are strongly encouraged to use LaTeX and the Springer "llncs" format, which can be obtained from the Springer Web site. Abstracts must be registered by Feb. 27, 2006. All submissions must be received by March 6, 2006. The proceedings of IJCAR 2006 will be published by Springer-Verlag in the LNAI/LNCS series.

    Logics of interest include propositional, first-order, classical, equational, higher-order, nonclassical, constructive, modal, temporal, many-valued, substructural, and description logics; metalogics; type theory; and set theory.

    Methods of interest include tableaux, sequent calculi, resolution, model-elimination, connection method, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, efficient data-structures and indexing, integration of computer algebra systems and automated theorem provers, and combination of logics or decision procedures.

    Applications of interest include hardware and software verification, formal methods, program analysis and synthesis, computer arithmetic, metatheory of languages and logics, declarative programming, deductive databases, knowledge representation, computer security, natural language processing, linguistics, robotics, and planning.

    Awards will be given for the best paper and for the best paper written solely by one or more students. The selection will be done by the program committee. A submission is eligible for the best student paper award if all authors are full-time students at the time of submission. The program committee may decline to make the awards or may split it among several papers.

    For further information, see the Web site.

    LARARL

    The CSR 2006 Workshop on Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL) will be held at the International Computer Science Symposium in Russia St. Petersburg, Russia, June 8-12, 2006. This workshop will bring together practioners and researchers who are concerned with the logics that underlie automated reasoning, and the use of automated reasoning to investigate logics and their applications. Reasoning in all forms (automated, interactive, etc.) and all logics (classical, nonclassical, all orders, etc.) is of interest to the workshop. The workshop will be divided into two tracks:

    Logic for Automated Reasoning

    Automated Reasoning for Logic

    Submission of papers (max. 20 pages) for presentation at the workshop, and proposals for system and application demonstrations at the workshop, are now invited. Full details of the workshop and submission requirements are on the Web page. Submission deadline is March 6, 2006.

    RWCA 2006

    On March 16-17, 2006, the tenth Rhine Workshop on Computer Algebra will be held in Basel, Switzerland. This informal workshop is held every other year and gives young researchers in all subfields of computer algebra an opportunity to present their work. Of particular interest to AAR members is the presentation by Jacques Calmet, whose specialty is computer algebra and deduction systems. Submissions are due December 15, 2005. For information, please see the Web page.

    TERMGRAPH 2006

    The Third International Workshop on Term Graph Rewriting will take place on April 1, 2006, in Vienna, Austria. The workshop will be collocated with ETAPS'06.

    Term graph rewriting is concerned with the representation of functional expressions as graphs and the evaluation of these expressions by rule-based graph transformation. Topics of interest range from theoretical questions to practical implementation issues, including the modeling of (finite or infinitary) first-order term rewriting by (acyclic or cyclic) graph rewriting, interaction nets and sharing graphs for Levy-optimal reduction in the lambda calculus, rewrite calculi on cyclic higher-order term graphs for the semantics and analysis of functional programs, graph reduction implementations of functional programming languages, and automated reasoning and symbolic computation systems working on shared structures. The deadline for submission is January 7, 2006. For more information see the Web page.

    PSI 2006

    "Perspectives of System Informatics" (PSI 2006) will be held June 27-30, 2006, in Novosibirsk, Akademgorodok, Russia. This conference is held to honor the 75th anniversary of academician Andrei Ershov (1931-1988) and his outstanding contributions in advancing informatics. The aim of the conference is to provide a forum for the presentation and in-depth discussion of advanced research directions in computer science. Improvement of the contacts and exchange of ideas between researchers from the East and West are further goals.

    Conference topics fall into three categories:

    Submission instructions can be found on the conference Web site. The submission deadline for extended abstracts is January 23, 2006.

    A book of extended abstracts of invited and accepted talks will be available at the conference. The full versions of the papers presented at the conference will be published by Springer-Verlag in the LNCS series after the conference.

    CAV 2006

    The 18th International Conference on "Computer Aided Verification" (CAV 2006) will be held in Seattle, Washington, August 16-21, 2006. This conference series is dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for hardware and software systems. This year, CAV is part of the 4th International Federated Logic Conference (FLoC 2006), which includes CAV and five other conferences/symposia. The first day of CAV is traditionally a tutorial day; this year, the tutorial will be replaced with a special symposium entitled "25 Years of Model Checking."

    There are two categories of submissions: regular papers (max. 13 pages) and tool presentations (max. 4 pages). Topics of interest include algorithms and tools for verifying models and implementations; hardware verification techniques; program analysis and software verification; modeling and specification formalisms; deductive, compositional, and abstraction techniques for verification; testing and runtime analysis based on verification technology; applications and case studies; verification in industrial practice. Submission deadline is January 27, 2006. For information concerning the procedure for submissions, check the conference home page.

    ESSLLI 2006 Student Session

    The Student Session of the 18th European Summer School in Logic, Language and Information (ESSLLI) will be held July 31 - August 11, in Malaga, Spain. The aim of the Student Session is to provide students with the opportunity to present their work in progress and get feedback from senior researchers and fellow-students. The ESSLLI Student Session invites students at any level, undergraduates as well as graduates, to submit a full paper, no longer than 7 pages (including references). Papers should be submitted with clear indication of the selected modality of presentation (i.e., oral or poster). Accepted papers will be published in the Student Session Proceedings. Papers should describe original, unpublished work, complete or in progress, that demonstrates insight, creativity, and promise. The deadline for submission is February 1, 2006. For more information about the Student Session, and for the technical details concerning submission, please visit the Web site, or contact one of the chairs: Janneke Huitink (j.huitink@phil.ru.nl) or Sophia Katrenko (katrenko@science.uva.nl).

    RTA'06

    The 17th International Conference on Rewriting Techniques and Applications (RTA'06) will be held August 12-14, 2006, in Seattle, Washington, as part of the Federated Logic Conference (FLoC), collocated with CAV, ICLP, IJCAR, LICS, SAT, and several affiliated workshops. Typical areas of interest include the following:

    Submission categories include regular research papers and system descriptions. Problem sets and submissions describing interesting applications of rewriting techniques are also welcome. The submission deadline is February 15, 2006, for abstracts and February 22, 2006, for full papers. Please see the Web site for details.

    An award is given to the best paper or papers. A limited number of travel grants may be available for students who are (co-)authors of RTA-papers.

    JELIA'06

    The 10th European Conference on Logics in Artificial Intelligence will be held in Liverpool, U.K., September 13-15, 2006. JELIA'06 will bring together researchers interested in all aspects concerning the use of logics in AI to discuss current research, results, problems and applications of both a theoretical and practical nature. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in AI.

    There are two categories of submission:

    1. Regular papers. Submissions should not exceed 13 pages including figures, references, and so forth and should contain original research, and sufficient detail to assess the merits and relevance of the contribution.

    2. Tool descriptions. Submissions should not exceed 4 pages, and should describe the implemented tool and its novel features. A demonstration is expected to accompany a tool presentation.

    Proceedings will be published by Springer-Verlag in the Lecture Notes on Artificial Intelligence series. All submissions must be received (in PS or PDF only) by May 1, 2006, and should be submitted via the form available at the JELIA-06 For further details, see Web page.

    Call for Nominations: Ackermann Award 2006

    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.

    The deadline for submission is December 31, 2006. Details about the award are available on the Web.

    Reasoning in Description Logics:
    Special Issue of the Journal of Automated Reasoning

    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:

    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.

    Electronic submissions (in postscript or pdf format) should be prepared by using the style files on the Web and should be sent to jar@tcs.inf.tu-dresden.de.

    Guest Editor

    Franz Baader (TU Dresden, Germany); http://lat.inf.tu-dresden.de/$\sim$baader/index-en.html

    For further information, please contact the guest editor by sending an email to jar@tcs.inf.tu-dresden.de.

    Important Deadlines

    Paper submission April 16, 2006
    Reviews due July 16, 2006
    Revised version due September 3, 2006
    Final reviews due October 1, 2006
    Final version due November 5, 2006
    Publication date March 2007


    Gail W. Pieper
    pieper@mcs.anl.gov
    December 2005