AARNEWS - December 2003

ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 61 Dec. 2003

From the AAR President
Results of the CADE Trustee Elections 2003
Herbrand Award: Call for Nominations
Call for Tutorial Proposals
Call for Papers

  • RTA'04
  • AISC 2004
  • WoLLIC'2004o
  • New Books
  • Reasoning about Uncertainty
  • Automated Reasoning and the Discovery of Missing and Elegant Proofs
  • From the AAR President, Larry Wos...

    I join Maria Paola in congratulating the new CADE trustees. And I am pleased to see that membership in CADE continues to increase. I would, however, like to see all our members contributing articles, problems, challenges---not only to the AAR Newsletter but also to the Journal of Automated Reasoning. Yes, I do mean "all": if we have to expand the journal and run more issues of the newsletter, marvelous.

    While I am making outrageous requests, let me add the following. Please flood me with information about how you are using OTTER: in education, program verification, protocol analysis---whatever.

    Results of the CADE Trustee Elections 2003

    Maria Paola Bonacina
    (Secretary of AAR and CADE) E-mail: mariapaola.bonacina@univr.it

    An election was held from September 26 through October 15, 2003, to fill three positions on the board of trustees of CADE Inc. The three positions were left vacant by Ulrich Furbach, Michael Kohlhase, and David McAllester, whose terms expired. Franz Baader, Peter Baumgartner, Michael Kohlhase, and Stephan Schulz were nominated for these positions (see AAR Newsletter No. 60, September 2003). Michael Kohlhase was nominated for a second term; Franz Baader was nominated for a first term as elected trustee, after one year as CADE 2003 Program Chair; and Peter Baumgartner and Stephan Schulz were nominated for a first term.

    Ballots were sent by electronic mail to all members of AAR as of September 26, for a total of 587 ballots (up from 566 in 2002, 548 in 2001, 445 in 2000, and 396 in 1999). Of these, 116 were returned with a vote, representing a participation level of 19.8% (down from 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 59.

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

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    F. Baader 48 26 17 25 116
    P. Baumgartner 32 42 21 21 116
    M. Kohlhase 28 24 25 39 116
    S. Schulz 8 23 39 46 116

    No candidate reaches a majority right away, and the redistribution of the votes of Stephan Schulz yields the following new distribution:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    F. Baader 49 32 33 2 116
    P. Baumgartner 35 49 29 3 116
    M. Kohlhase 31 30 51 4 116

    Again, no candidate reaches a majority, and by redistributing the votes of Michael Kohlhase one gets the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    F. Baader 64 47 5 0 116
    P. Baumgartner 50 60 6 0 116

    Thus, Franz Baader has a majority of preferences and is elected for a first term as elected trustee. The redistribution of the votes of the winner produces the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    P. Baumgartner 60 31 23 2 116
    M. Kohlhase 39 32 42 3 116
    S. Schulz 17 44 53 2 116

    Peter Baumgartner has a majority right away and is elected. Redistributing Peter Baumgartner's votes, one obtains the following matrix:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    M. Kohlhase 64 48 3 1 116
    S. Schulz 47 62 7 0 116

    There is a majority of preferences for Michael Kohlhase, who is elected.

    In the weeks following the elections, the Board of Trustees elected Frank Pfenning and Andrei Voronkov as president and vice-president, respectively, of CADE Inc., resulting in the following list of CADE Trustees:

    Franz Baader (Past program chair, elected 10/2003)
    David Basin (IJCAR 2004 Program co-chair)
    Peter Baumgartner (Elected 10/2003)
    Maria Paola Bonacina (Secretary)
    Gilles Dowek (Elected 9/2001)
    Harald Ganzinger (Past program chair, elected 10/1999 and 10/2002)
    John Harrison (Elected 9/2001)
    Michael Kohlhase (Elected 10/2000 and 10/2003)
    Neil V. Murray (Treasurer)
    Frank Pfenning (President, elected 10/1998 and 9/2001)
    Andrei Voronkov (Vice-President, past program chair, elected 10/2002)
    Toby Walsh (Elected 10/2002)

    On behalf of the AAR and CADE Inc., I thank Ulrich Furbach, for his service as trustee and CADE Inc. president during the past six years; David McAllester, for his service as trustee during the past three years; Stephan Schulz, for running in the election; and all the members who voted, for their participation; and I offer the warmest congratulations to Franz Baader, Peter Baumgartner, and Michael Kohlhase on being elected trustees and to Frank Pfenning and Andrei Voronkov on being elected president and vice-president, respectively, of CADE Inc.

    Herbrand Award: Call for Nominations

    Maria Paola Bonacina
    Secretary of AAR and CADE
    On behalf of the CADE Inc. Board of Trustees

    The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

    Larry Wos (1992)
    Woody Bledsoe (1994)
    Alan Robinson (1996)
    Wu Wen-Tsun (1997)
    Gerard Huet (1998)
    Robert S. Boyer and J Strother Moore (1999)
    William W. McCune (2000)
    Donald W. Loveland (2001)
    Mark E. Stickel (2002)
    Peter B. Andrews (2003)

    A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at IJCAR 2004 is

    April 1, 2004
    Nominations pending from previous years must be resubmitted in order to be considered.

    Nominations should consist of a letter (preferably email) of up to 2000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2000 words of endorsement from two other seconders. Nominations should be sent to

    Frank Pfenning
    President of CADE Inc.
    fp@cs.cmu.edu
    with copies to mariapaola.bonacina@univr.it.

    Call for Tutorial Proposals - IJCAR 2004

    The International Joint Conference on Automated Reasoning (IJCAR 2004) will take place July 4-8, 2004, in Cork, Ireland. This second IJCAR will merge CADE, FTP, TABLEAUX, FroCoS (Workshop on Frontiers of Combining Systems), and CALCULEMUS (Symposium on the Integration of Symbolic Computation and Mechanized Reasoning).

    Tutorials for IJCAR 2004 will be held on July 4-5, 2004. They may run a half-day or full day. An IJCAR tutorial can be on any IJCAR-related topic. (Examples of IJCAR areas of interest can be found in the IJCAR Call for Papers at the Web.) The following kinds of tutorials are especially desirable:

    Interested readers should sent a two- to three-page proposal to the tutorial chair (wmfarmer@mcmaster.ca) no later than February 1, 2004. The proposal should be in plain text, postscript, or PDF format and should contain the following information:

    1. Title of the tutorial.

    2. Short biographical description of the presenter(s) of the tutorial that includes name, affiliation, contact information, and relevant background.
    3. Description of the tutorial. Is the duration of the tutorial a half day or a full day? What date is preferred (July 4 or 5)? Are there any special equipment requirements?
    4. Intended audience. How many participants are expected? Is there any sort of limitation to participation?

    Tutorial participants are not required to register for IJCAR 2004. Tutorial organizers must, however, create and maintain a Web page that describes the tutorial for the IJCAR community. The IJCAR organizers offer to copy and distribute tutorial notes to registered tutorial participants. All questions concerning tutorials should be directed to the tutorial chair William Farmer (wmfarmer@mcmaster.ca).

    Call for Papers

    RTA'04

    The 15th International Conference on Rewriting Techniques and Applications (RTA'04) will be held June 3-5, 2004, as part of the Federated Conference on Rewriting, Deduction and Programming (RDP'04). RTA is the major forum for the presentation of research on all aspects of rewriting. Typical areas of interest include the following:

    Invited talks will be given at RTA'04 by Neil Jones (Copenhagen), Aart Middeldorp (Innsbruck), and Robin Milner (Cambridge).

    Interested researchers are invited to submit a paper. The deadlines are January 15, 2004, for electronic submission of title and short abstract, and January 22, 2004, for electronic submission of the full paper. Submissions must be original and not submitted for publication elsewhere. Submission categories include regular research papers and system descriptions. Problem sets and submissions describing interesting applications of rewriting techniques are also welcome.

    Accepted papers will appear in the Springer-Verlag Lecture Notes in Computer Science series. More information about paper submission will be available at the RDP'04 Web.

    A 1000 Euro award will be given to the best paper or papers as decided by the program committee. The award may also totally or partially go to the best paper with a student as main author, according to the submission letter.

    For further details please contact the program chair:

    Vincent van Oostrom
    Universiteit Utrecht
    Department of Philosophy
    Heidelberglaan 8
    3584 CS Utrecht, Netherlands
    Vincent.vanOostrom@phil.uu.nl

    AISC 2004

    The Seventh International Conference on Artificial Intelligence and Symbolic Computation will take place September 22-24, 2004, at the Research Institute for Symbolic Computation, Castle of Hagenberg, Austria.

    Artificial intelligence and symbolic computation are two views and approaches for automating problem solving, in particular mathematical problem solving. The two approaches are based on heuristics and on mathematical algorithmics, respectively. Artificial intelligence can be applied to symbolic computation and vice versa; hence, a wealth of challenges, ideas, theoretical insights and results, methods, and algorithms arise in the interaction of the two fields and research communities. Advanced tools of software technology and system design are needed, and a broad spectrum of applications is possible by the combined problem solving power of the two fields.

    Researchers working in artificial intelligence, symbolic computation, computer algebra, automated theorem proving, and automated reasoning are invited to share their views, work, and results by submitting papers and participating in the conference. Papers should be submitted by May 1, 2004. The proceedings of the conference containing the refereed and accepted papers will appear as a volume of the Springer-Verlag Lecture Notes. For details see the Web.

    WoLLIC'2004

    The 11th Workshop on Logic, Language, Information and Computation will take place in Paris July 19-22, 2004. The aim of the workshop is to foster interdisciplinary research in pure and applied logic.

    Contributions are invited in the form of short papers (12 A4 10pt pages) in all areas related to logic, language, information, and computation. The papers should be sent preferably in postscript format by e-mail to wollic@cin.ufpe.br. Submissions must be received by one of the co-chairs of the organizing committee by March 1, 2004. Papers must be anonymous: A separate identification page must be included. The papers must be written in English and give enough detail to allow the program committee to assess the merits of the work. Papers should start with a brief statement of the issues, a summary of the main results, and a statement of their significance and relevance to the workshop. References and comparisons with related work are also expected. Technical development directed to the specialist should follow. Results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. One author of each accepted paper will be expected to attend the conference in order to present the paper. Authors will be notified of acceptance by April 1, 2004.

    The proceedings will appear as a volume in the Elsevier series Electronic Notes in Theoretical Computer Science. Full versions of papers will be refereed again for publication in a special issue of the Logic Journal of the IGPL.

    ASL sponsorship of WoLLIC'2004 also will permit student ASL members to apply for (limited) ASL travel funds that we hope to make available for sponsored meetings that take place in 2004 In addition, WoLLIC'2004 will make available modest grants to graduate students in logic and to recent Ph.D.'s so that they may attend the meeting in Paris. To be considered for a grant, please (1) send a letter of application, and (2) ask your thesis supervisor to send a brief recommendation letter. The application letter should be brief (one page) and should include (1) your name, (2) your home institution, (3) your thesis supervisor's name, (4) a one-paragraph description of your studies and work in logic, (5) your estimate of the travel expenses you will incur, (6) (for citizens or residents of EU) citizenship or visa status, and (7) (voluntary) indication of your gender and minority status. Only modest grants will be possible, partially covering travel costs and perhaps some of the living expenses during the meeting. Women and members of minority groups are strongly encouraged to apply. Application by e-mail is encouraged; put "WoLLIC grant application" in the subject line of your message. Applications and recommendations should be received before the deadline of March 1, 2004, by one of the co-chairs of the organizing committee.

    For further information, contact one of the co-chairs of the organizing committee:

    Patrick Cegielski
    Université Paris 12-IUT
    Département Informatique
    Route Forestière Hurtault
    F-77300 Fontainebleau, France
    Tel: +33.(0)1.60.74.68.16 (office)
    Fax: +33.(0)1.60.74.68.28
    E-mail: cegielski@univ-paris12.fr

    Ruy de Queiroz
    Centro de Informatica
    Univ. Fed. Pernambuco
    Av. Prof. Luis Freire, s/n, 50740-540 Recife, PE, Brazil
    Tel: +55 81 3271 9430
    Fax: +55 81 3271 9438
    E-mail: ruy@cin.ufpe.br

    Or, see the Web.

    New Books

    Reasoning about Uncertainty, by Joseph Y. Halpern

    Uncertainty is a fundamental and unavoidable feature of daily life; in order to deal with uncertainty intelligently, we need to be able to represent it and reason about it. In this book Joseph Halpern examines formal ways of representing uncertainty and considers various logics for reasoning about it. While the ideas presented are formalized in terms of definitions and theorems, the emphasis is on the philosophy of representing and reasoning about uncertainty; the material is accessible and relevant to researchers and students in many fields, including computer science, artificial intelligence, economics (particularly game theory), mathematics, philosophy, and statistics. Halpern begins by surveying possible formal systems for representing uncertainty, including probability measures, possibility measures, and plausibility measures. He considers the updating of beliefs based on changing information and the relation to Bayes' theorem; this leads to a discussion of qualitative, quantitative, and plausibilistic Bayesian networks. He considers not only the uncertainty of a single agent but also uncertainty in a multiagent framework. Halpern then considers the formal logical systems for reasoning about uncertainty. He discusses knowledge and belief; default reasoning and the semantics of default; reasoning about counterfactuals, and combining probability and counterfactuals; belief revision; first-order modal logic; and statistics and beliefs. He includes a series of exercises at the end of each chapter.

    456 pp., cloth, ISBN 0-262-08320-5, US$50
    For more information see the
    Web.

    Automated Reasoning and the Discovery of Missing and Elegant Proofs
    by Larry Wos and Gail W. Pieper

    This book is rare--perhaps the only one of its type--in that it simultaneously provides the basis for diverse courses in logic, mathematics, and automated reasoning; teaches how research can be successfully conducted; and presents results that had eluded various masters for many decades. Key to obtaining these results is the use of strategies and methodologies, detailed in this volume, and the program OTTER--which automates logical reasoning, deducing millions of conclusions that follow inevitably from the hypotheses supplied by the user. In this book, various aspects of the newly discovered Hilbert's twenty-fourth problem are addressed. The included CD-ROM offers OTTER in various forms, numerous input files, and a large number of proofs that are new. By experimenting with these offerings, both the new researcher and the expert alike may experience the excitement of attacking deep open questions and discovering missing and elegant proofs.

    384 pp., with CD-ROM, hardcover, ISBN 1-58949-023-1, US$88
    For more information see the
    Web.


    Gail W. Pieper
    Technical editor
    December 2003