AARNEWS - September 2002



No. 56, September 2002


From the AAR President
Second IJCAR to Be Held in 2004
Announcement of the 2002 Herbrand Award
News from the Secretary
Announcement of CADE Elections
Thesis Abstracts

  • On the Integration of Decision Procedures in Automated Deduction
  • Checking Validities and Proofs with CVC and flea

  • Call for Papers
  • CADE-19
  • LICS 2003

  • Logic and Automated Reasoning Summer School
    Book Announcement
    Special Issues
  • Bytecode Verification
  • Automated Reasoning and Theorem Proving in Education
  • From the AAR President, Larry Wos...

    Good researchers not only develop novel strategies, implement powerful programs, and conduct numerous experiments, but they also keep the community informed about their accomplishments. This newsletter features a number of calls for papers or for contributions to special issues. I encourage you all to take advantage of these opportunities and to make your research results widely known.

    Second International Joint Conference on
    Automated Reasoning to be held in 2004

    Maria Paola Bonacina

    After several years of gradual fragmentation of the Automated Reasoning community into various conferences and workshops, the CADE/AAR, FTP and TABLEAUX communities decided to have a joint conference, the International Joint Conference on Automated Reasoning (IJCAR), held in Siena (Italy), June 18-23, 2001.

    IJCAR 2001 was regarded as a clear success and the IJCAR Business Meeting in Siena voted overwhelmingly to have a second IJCAR. In the fall of 2001, the CADE Inc. Board of Trustees, the FTP Steering Committee and the TABLEAUX Steering Committee agreed to have the Second International Joint Conference on Automated Reasoning in 2004, welcoming also the Workshop on Frontiers of Combining Systems (FroCoS). In the summer of 2002, the Calculemus Symposium, which had already co-located with IJCAR 2001, also joined IJCAR proper.

    General Agreement

    The CADE board of trustees and the steering committees of Calculemus, FroCoS, FTP, TABLEAUX, respectively, agree to the following:

    Basic Statement: CADE, Calculemus, FroCoS, FTP and TABLEAUX agree to have IJCAR together and IJCAR will replace these events in 2004.

    Conference Chair and Location: Toby Walsh, University College Cork, Cork, Ireland.

    Program Committee: IJCAR 2001 had three program co-chairs, designated by its constituent meetings, respectively. In order to foster integration, IJCAR 2004 will have two program co-chairs, selected as follows: the CADE board of trustees and the steering committees of Calculemus, FroCoS, FTP, TABLEAUX, respectively, will make up to two nominations each. The IJCAR steering committee will propose two names out of the slate of all nominees from the constituent meetings, and ask the latter to accept them or suggest motivated changes, till a reasonable consensus is reached in reasonable time. This procedure was also presented at the Business Meetings of CADE and Tableaux during FLoC 2002 and met no objection.

    Program: Similar to 2001, it is expected that the program co-chairs will choose a balanced program committee with significant representation from all participating communities, and the scope of the joint conference will be at least the union of the scopes of the constituent meetings. IJCAR will invite submission related to all aspects of automated reasoning, including foundations, implementations, and applications.

    Proceedings: As in 2001 there will be one common set of proceedings and the editors will be the two program co-chairs.

    Other officers: The program co-chairs will appoint workshop chair, tutorial chair and publicity chair, possibly in consultation with the steering or program committee. The conference chair may appoint a treasurer, possibly in consultation with the steering committee, and a local arrangements chair or committee at his discretion.

    IJCAR Steering Committee: IJCAR 2001 had a steering committee formed of the conference chair, the three program co-chairs and up to two representatives per constituent meeting. In order to accomodate the new entries while keeping the committee's size reasonable, the IJCAR 2004 steering committee will include the following: the IJCAR conference chair, the previous IJCAR conference chair (for continuity), the two IJCAR program co-chairs, and one representative per constituent meeting.

    At present, this results in the following list:

    Alessandro Armando (FroCoS), Christoph Benzmueller (Calculemus), Maria Paola Bonacina (FTP), Ulrich Furbach (CADE), Reiner Haehnle (Tableaux), Fabio Massacci (former conference chair), Toby Walsh (conference chair), with the two program co-chairs yet to be determined, and Maria Paola Bonacina as coordinator.

    Finances: CADE Inc. will back financially IJCAR 2004 at the same conditions of 2001: in case of loss, CADE Inc. bears the loss; in case of profit, the revenue goes into the CADE Inc. account, with 25% earmarked to support future CADEs, and 75% earmarked to support future IJCARs.

    Comments and suggestions from all members of the AAR community are very welcome and will be carefully listened to.

    The Committees Supporting IJCAR 2004

    CADE Trustees (CADE-board@sci.univr.it): Franz Baader (CADE 2003 program chair), Maria Paola Bonacina (Secretary), Gilles Dowek, Ulrich Furbach (President), Harald Ganzinger (outgoing), John R. Harrison, Michael Kohlhase, David McAllester, Neil V. Murray (Treasurer), Frank Pfenning (Vice-President), David A. Plaisted (outgoing), Andrei Voronkov (CADE 2002 program chair: outgoing).

    Calculemus Trustees: Michael Beeson, Wolfgang Windsteiger, James Davenport, Alessandro Armando, Steve Linton, Roberto Sebastiani, Volker Sorge, Olga Caprotti, Therese Hardin, Renaud Rioboo, Andrzei Trybulec, Silvio Ranise.

    FroCoS Steering Committee (frocos-sc@mrg.dist.unige.it): Alessandro Armando, Franz Baader, Christoph Ringeissen, Klaus U. Schulz.

    FTP Steering Committee (ftp-sc@logic.at): Alessandro Armando, Peter Baumgartner, Maria Paola Bonacina (President), Ricardo Caferra, Domenico Cantone, David Crocker, Ingo Dahn, Bernhard Gramlich, Reiner Haehnle, Alexander Leitsch, Paliath Narendran, Christoph Weidenbach.

    TABLEAUX Steering Committee (reiner@cs.chalmers.se): Marcello D'Agostino, Uwe Egly, Chris Fermüller, Melvin Fitting, Ulrich Furbach, Didier Galmiche, Rajeev Gore, Reiner Haehnle (President), Fabio Massacci, Peter H. Schmitt (Vice-President).

    Announcement of the 2002 Herbrand Award

    Mark E. Stickel was awarded the Herbrand Award at CADE 2002 for for his ground-breaking discoveries in AC-unification, reasoning modulo a theory, term indexing, and thorough development of the SNARK and PTTP provers, as well as many other contributions to the field of automated reasoning.

    Announcement of CADE Elections

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

    An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people are currently serving as Trustees of CADE Inc.:

    Franz Baader (CADE 2003 Program Chair)
    Maria Paola Bonacina (Secretary)
    Gilles Dowek (elected 9/2001)
    Ulrich Furbach, President (elected 8/1997 and re-elected 10/2000)
    Harald Ganzinger (past Program Chair, elected 10/1999: term expired)
    John R. Harrison (elected 9/2001)
    Michael Kohlhase (elected 10/2000)
    David McAllester (past Program Chair, elected 10/2000)
    Neil V. Murray (Treasurer)
    Frank Pfenning, Vice-President (elected 10/1998 and re-elected 9/2001)
    David A. Plaisted (elected 10/1999: term expired)
    Andrei Voronkov (CADE 2002 Program Chair: term expired)

    The terms of office of Harald Ganzinger and David Plaisted are expiring, because CADE trustees are elected to serve for three years, as well as that of Andrei Voronkov. The position of Andrei Voronkov is replaced by Franz Baader, as CADE 2003 Program Chair. Nonetheless, there are three positions to fill, because CADE Inc. is implementing the amendment to its bylaws, approved by the membership in the summer of 2000, that requires to increase the number of trustees from nine to twelve, by electing three trustees instead of two for three elections. The first two elections with an additional slot were held in 2000 and 2001, and this is the third such election (see AAR Newsletter No. 48, August 2000).

    The following candidates were nominated:

  • Harald Ganzinger (http://www.mpi-sb.mpg.de/~hg/), nominated by Chris Lynch and Franz Baader
  • Jean Goubault-Larrecq (http://www.lsv.ens-cachan.fr/~goubault/), nominated by Gilles Dowek and John Harrison
  • Reinhold Letz (http://www4.in.tum.de/~letz/), nominated by Stephan Schulz and Don Loveland
  • Andrei Voronkov (http://www.cs.man.ac.uk/~voronkov), nominated by David Plaisted and Bill McCune
  • Toby Walsh (http://4c.ucc.ie/~tw), nominated by Alan Bundy and Michael Kohlhase
  • and provided the following statements.

    Statement by Harald Ganzinger

    CADE is the major forum for the scientific exchange of new theoretical and practical approaches to automated theorem proving and its applications in mathematics and computer science. In order to maintain high visibility of the field as a whole, we have to try to keep CADE's spectrum as wide as possible and to avoid any fragmentation of the field (and of CADE) into small subcommunities with too narrow methods and techniques. During the last three years as CADE trustee I have helped in re-uniting our community and in creating IJCAR01 which turned out to be a very successful event, convincingly demonstrating the high quality and relevance of our field. I will try to establish IJCAR as a regular event with even more communities, in particular from major areas of application of automated deduction, join us.

    On the other side, CADE needs to remain well embedded into its neighboring disciplines both on the theoretical side (logic in computer science, term rewriting) and on the practical side (verification, knowledge representation, logic programming, computer algebra). As CADE trustee I would continue to pursue the tasks implied by this view. Here is where my new role as FLoC General Chair would interact with my role as CADE trustee. That interaction, I believe, would be fruitful for both CADE and FLoC.

    Apart from these political issues that I can't escape at my age my heart is still beating for research. And consequently I remain seeing it as one of my main tasks to help maintaining the high scientific standards of the CADE conferences. Research presented at CADE should not be classified as theoretical or practical or applied, it should only be classified as good or bad, and excellency should be the only criterion according to which we decide what is CADE and what it is not.

    Statement by Jean Goubault-Larrecq

    To the man-in-the-street, automated reasoning is a theoreticians' business. Whilst that may be true, automated reasoning has acquired credentials in becoming central in many application domains: software certification with proof assistants, description logics and the semantic Web, decidable classes of first-order logic and tree automata applied to cryptographic protocol verification are a few examples that come to mind.

    I feel it is important that the automated reasoning community remains cohesive, despite the multitude of conferences on the topic (among which CADE, Tableaux, FTP, TPHOLs, RTA, LPAR). To this end, the idea of a periodic, but not annual, IJCAR conference seems to be a good way of getting people from all branches of automated reasoning to meet from time to time.

    It is is equally important that automated reasoning displays its value in applications, and more generally its many links with other domains of logics, mathematics, and philosopy. In this respect, I will favor the move to have CADE associated workshops---which, as far as I know, were introduced this year in the context of FLoC, and should be continued even independently of FLoC.

    During my career, I have been interested in several aspects of logic: automated reasoning in classical logic to begin with, then lambda-calculi, modal and intuitionistic logics, and then first-order logic again, in particular the relationship between decidable subclasses and finite tree automata. I am convinced that automated reasoning is not only a rich domain but also still a very promising one in many respects. If elected, I'll make every effort to promote it and its leading conference, CADE.

    Statement by Reinhold Letz

    Although the automated reasoning community is relatively stable, in the last years CADE suffers from a continuous decrease in the numbers of submissions and participants. Broadening of the scope is certainly one possible remedy, another is the collocation or the merging with other conferences, as worked successfully with IJCAR and should definitely be continued.

    But I think this is not enough, we also need new paradigms. As an example, consider fully automated proof search for first-order logic, where I am most competent. This important subfield of automated reasoning seems completely closed. There is a small number of sophisticated high-performance systems, newcomers have no chance to enter and consequently new paradigms cannot arise. Yet it should be clear to anybody that with the general approach of those systems (organising proof search on the microscopic level of single inferences) really hard problems cannot be solved fully automatically, even if we increase the performance by magnitudes. As a trustee I would try to act in the direction that new interesting ideas which conflict with the standard approaches can be presented.

    I want to conclude with something completely different. I am fully aware that in the organisation of a conference inevitably certain compromises have to me made, but nevertheless I think that it is not a law of nature that scientists have to eat bad food.

    Statement by Andrei Voronkov

    In the recent years automated deduction developed into a mature field. In traditional topics in deduction, such as resolution theorem proving, obtaining new results is becoming increasingly difficult. At the same time, there are very interesting areas where the methods of automated deduction used extensively. As a consequence, there have been a considerable shift of interest in automated deduction, as can be witnessed by a change in topics of the papers accepted to CADE and the success of newer meetings related to deduction, such as TPHOL, Calculemus, and Tableaux. My point of view on the future of CADE is as follows:
  • CADE will remain the conference in automated deduction.
  • CADE should not try to subsume other conferences in the area but should rather co-exist with them. IJCAR is an interesting meeting and should be continued but not on the annual basis. If we try to merge automated reasoning conferences into one large conference, there will be a little chance, especially for younger people, to publish papers and this may cause the shift of people to other areas (and the break-away conference will emerge anyhow).
  • CADE should broaden its scope and attract more submissions in new areas and application-related areas, for example verification, description logics, knowledge bases etc.
  • It seems to me that in the last years too many good papers have been rejected from CADE. I believe that CADE should accept more papers.
  • Automated reasoning is one of the most fundamental areas in computing. Its main niche in computer science and mathematics is to support other areas (formal methods, verification, compilers, proof assistants, constraints, PCC etc.) There is usually a layer between automated deduction tools and techniques and the target application. As a result, the efforts of people working in deduction remain unnoticed which results in unpleasant side-effects, such as difficulties in getting university positions at all levels. It is my firm opinion that the area should be better advertised and popularised outside the community than it is now.
  • Statement by Toby Walsh

    The automated reasoning (AR) community faces a number of fundamental problems. First, there is increasing fragmentation. Events like IJCAR (which I am proposing to host in Cork in 2004) are one solution to this problem. However, we cannot stop there but must embrace other closely related areas (for example, we need to join with the satisfiability research community, in which I am very active) that have common research problems. Second, there must be more fresh blood brought into the field. I hope, for example, that we can run a doctoral programme alongside IJCAR to engage PhD students at an early stage in their studies. Third, we need to take measures to prevent research in AR become stale and incremental. As area chair in automated reasoning for CologNet, I am responsible for organizing meetings at events like CADE and IJCAR to identify grand challenges for AR. The hope is that these challenges will fire the imaginations of both new researchers arriving into AR as well those already long established in the field.

    Brief bio: Toby Walsh recently moved to University College Cork as SFI Research Professor and Deputy Director of the Cork Constraint Computation Centre. He was previously an EPSRC advanced research fellow at the University of York. He completed his Ph.D. in automated reasoning at the University of Edinburgh under the supervision of Profs. Alan Bundy and Fausto Giunchiglia.

    News from the Secretary

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

    Over the summer I moved from the University of Iowa to the Università degli Studi di Verona, so that the AAR has now a home in Verona, Italy, in addition to its first home at the Argonne National Laboratory with AAR President Larry Wos and AAR Newsletter Editor Gail Pieper. It follows that the CADE Board of Trustees has a new e-mail address at


    As far as membership is concerned, our association continues doing very well with 578 members (as of September 12, 2002) up from 553 of last year. CADE-18, held as part of the Federated Logic Conference 2002 in Copenhagen, Denmark, brought 40 new AAR members, out of 126 registered participants. The list of members is available on the Web, reachable from the AAR home page, and directly at the Web site.

    All members are encouraged to consult this list, and send by e-mail corrections and additions, especially the url of their home page, if missing. The list of members on the Web will be updated at least once per year, as time permits.

    Thesis Abstracts

    Title of Thesis 1:

    On the Integration of Decision Procedures in Automated Deduction

    Author: Silvio Ranise

    Institution: LORIA & INRIA-Lorraine

    Current Web page: http://www.loria.fr/~ranise

    Abstract: The thesis proposes three techniques to build reasoning specialists, to widen their scope, and to incorporate them in the simplification process of many verification systems.

    The first contribution is a uniform methodology to build satisfiability procedure for theories which extends the theory of equality and can be axiomatized by clauses. The methodology is developed in the rewriting framework which allows us to use a standard (refutation complete) superposition-based inference system for clausal equational logic. This allows us not only to handle pure equality but also several interesting axiomatic theories that were not handled previously that way such as lists, extensional arrays, and finite sets with extensionality. The proof that the decision procedures are correct is straightforward w.r.t. other correctness proofs given in the literature. In our approach, deriving satisfiability procedures for combination of theories is also immediate.

    The second contribution is a technique to extend the capabilities of reasoning specialists so that they can be linked with general-purpose verification system in a productive way. More precisely, given a satisfiability procedure for a class of formulae C, we describe how to widen its scope so that the satisfiability problem of a class C', which is a superset of C, can be (semi-)decided by the available procedure for C. The key ingredient of the extension schema is a lemma speculation mechanism that `reduces' the satisfiability problem of C' to the satisfiability problem of C. The schema enjoys basic theoretical properties such as soundness and termination.

    The third contribution is a (tight) integration schema between conditional rewriting and a satisfiability procedure. Rewriting is one of the most important formula simplification mechanism for theorem provers. The key observation is that contextual rewriting can be obtained by combining traditional conditional rewriting with a procedure capable of deciding whether any given literal is entailed by the context and normalizing expressions w.r.t. the information available in the context. Furthermore the pattern of interaction between rewriting and the procedure does not depend on the theory decided by the procedure. Constraint Contextual Rewriting (CCR, for short) is then the result of abstracting contextual rewriting from the theory decided by the decision procedure employed. An implementation of CCR, called Rewrite and Decision Procedure Laboratory (RDL), is described together with the experimental results on a corpus of significant problems extracted from the literature.

    Title of Thesis 2:

    Checking Validities and Proofs with CVC and flea

    Author: Aaron Stump

    Institution: Stanford University

    Date submitted: August 2002

    Current Web page: http://www.cs.wustl.edu/ stump/

    Abstract: In automated reasoning, decision procedures are algorithms capable of reporting whether or not a formula is logically valid. Decision procedures are fundamental tools for formal verification and other applications. This thesis describes solutions to theoretical and engineering problems arising in the development of the CVC (``Cooperating Validity Checker'') decision procedure. CVC implements a framework that allows independent decision procedures for the quantifier-free consequences of different logical theories to be combined. Assuming certain properties of those decision procedures, the combination results in a sound and complete decision procedure for the quantifier-free consequences of the combined theory. There are currently decision procedures implemented for theories of arrays, linear real arithmetic, and inductive data types. See the CVC Web page.

    The thesis begins with an overview of the internals of CVC. Then CVC's array decision procedure is described. This is the first published procedure for its theory, which subsumes similar theories previously decided in the literature. Next, an approach is described for handling partial functions. The approach is based on a theorem reducing validity in a logic of partial functions to validity in classical logic. Then proof production in CVC is considered. CVC has the ability to produce a proof for every formula it reports to be valid. These proofs are produced in a proof meta-language based on the Edinburgh Logical Framework (LF). The proofs can be checked by a proof checker called flea. Several new language features are supported in flea that make it much easier to produce proofs from CVC. Also, flea implements new optimizations to the basic LF type-checking algorithm to be able to check the large proofs produced by CVC for large input formulas. Empirical results showing the benefits of the optimizations are presented. Finally, several uses of proofs beyond certifying correctness of CVC's results are described, including a technique which extracts information from proofs to feed back to CVC's propositional reasoning engine, the Chaff SAT solver, for improved performance.

    Book Announcement

    Isabelle/HOL: A Proof Assistant for Higher-Order Logic
    by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel

    Springer LNCS 2283, ISBN 3-540-43376-7
    Web site

    This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts:

    1. Elementary Techniques shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion.

    2. Logic and Sets presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes Isabelle/HOL's treatment of sets, functions, and relations and explains how to define sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.

    3. Advanced Material describes a variety of other topics. Among these are the real numbers, records, and overloading. Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an extended example: the verification of a security protocol.

    Special Issues of the Journal of Automated Reasoning

    1. Bytecode Verification

    We are seeking articles on Bytecode Verification for a special issue of the Journal of Automated Reasoning.

    Topics: Bytecode verification for the Java Virtual Machine and related approaches to program analysis of low-level code for the enforcement of safety properties. Particularly welcome are contributions emphasizing the correctness of the analysis and the application of automated or interactive verification techniques.

    Submissions: Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.

    Deadline for submissions: October 13, 2002.

    Guest editor: Tobias Nipkow (nipkow@in.tum.de)

    For further information see the Web site.

    2. Automated Reasoning and Theorem Proving in Education (ARTE)

    During the past ten years, theorem proving has been playing an increasingly important role in education. One reason is the improvement in the "friendliness" of theorem provers; many are now suitable for the nonspecialist and produce quite readable proofs. Another is their demonstrated success in solving not only "toy" problems but previously open questions in mathematics and logic . In light of these developments, we plan a special issue of the Journal of Automated Reasoning, ARTE, on the use of theorem provers in education at all levels.


    Deepak Kapur, University of New Mexico


    Possible topics include the following:

  • Automated reasoning for mathematics and logic education
  • Mathematical tutoring
  • Geometry and theorem proving
  • Business education, statistics, and theorem proving
  • Theorem provers developed specifically for teaching
  • Educational games and theorem proving
  • Comparisons of theorem provers and symbolic systems
  • Web-based theorem provers for learning over the Internet
  • Automated courses
  • Theorem provers and education -- whence and whereto
  • We welcome contributions about experiences using automated theorem provers for education at all levels: from elementary and secondary school to college and university and beyond.

    Our focus is not on the use of theorem provers in classes specifically devoted to the teaching of theorem proving or automated reasoning. Rather, we are especially interested in discussion of the benefits (or problems encountered) in using automated theorem proving technology to motivate students and to enhance their ability to understand new topics.

    Prospective contributors are welcome to contact the editor to discuss the suitability of topics and papers.


    Please send 3 copies of your manuscript or (preferably) a postscript file to

    Dr. Deepak Kapur
    Chairperson, Computer Science Department
    University of New Mexico
    Albuquerque, NM 87131
    E-mail: kapur@cs.unm.edu
    Please also send one copy to
    Dr. Gail W. Pieper
    Managing Editor, Journal of Automated Reasoning
    Mathematics and Computer Science Division
    Argonne National Laboratory
    Argonne, IL 60439
    E-mail: pieper@mcs.anl.gov


    Submission deadline: December 10, 2002
    Notification: May 10, 2003

    Call for Papers

    CADE 19

    The 19th International Conference on Automated Deduction (CADE-19) will be held in Miami, Florida, USA, July 28 - August 2, 2003.

    CADE-19 invites paper submissions related to all aspects of automated deduction, including foundations, implementations, and applications. Original research papers, papers on applications of automated deduction methods and systems, and descriptions of working automated deduction systems are solicited.

    In addition, CADE-19 invites the submission of proposals for workshops and tutorials, which will take place at the beginning of the conference (July 28 and 29).


    Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory.

    Methods of interest include saturation, resolution, tableaux, sequent calculi, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, natural deduction, proof planning, proof presentation, proof checking, and explanation.

    Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI.


    Conference submission is electronic in postscript format. Submitted papers should conform to the Springer LNCS style. In addition to papers on foundations (15 pages), CADE encourages the submission of application papers (10 pages), and of short system descriptions (5 pages). Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. In the case of doubts on this point please contact the program chair. Papers that are too long will not be considered.

    Important Dates

    December 15, 2002: Deadline for submission of workshop and tutorial proposals
    January 15, 2003: Notification of acceptance of workshops and tutorials
    January 24, 2003: Deadline for electronic submission of title and short abstract
    January 31, 2003: Deadline for electronic submission of papers
    March 31, 2003: Notification of acceptance of papers
    April 30, 2003: Deadline for final version of accepted papers

    Conference Chairs: Geoff Sutcliffe (University of Miami, USA) and Jeff Pelletier (University of Alberta, Canada)

    Program Chair: Franz Baader (TU Dresden, Germany)

    More details will soon be available on the conference Web page.

    LICS 2003

    The Eighteenth IEEE Symposium on Logic in Computer Science will be held in Ottawa, Ontario, June 22-25, 2003. The organizers have made arrangements for pre- and post-LICS workshops to be run in conjunction with the main conference. Possible dates are 21st June and 26-27th June.

    Researchers and practitioners are invited to submit proposals for workshops on topics relating logic -- broadly construed -- to computer science or related fields. Funding is available to help defray the costs of a limited number of workshops.

    Proposals should include the following:

    Proposals are due Nov. 1, 2002, and should be submitted electronically to Prakash Panangaden, Workshops Chair LICS'03 (prakash@cs.mcgill.ca).

    For further information, see the LICS Web site.

    Logic and Automated Reasoning Summer School

    As computers become more powerful, their ability to perform complicated reasoning tasks increases. To harness their power, we need to understand the reasoning they do, and how they may do it more efficiently. This understanding begins with logic.

    The Australian National University (ANU) has an exciting opportunity for IT professionals, senior educators, and students to enhance their logic and reasoning skills for the workforce, for teaching, or for higher degree by research study, in a two-week intensive summer school at the ANU.

    The Logic and Automated Reasoning Summer School, to be held on 2-13 December 2002, comprises a blend of practical and theoretical short courses on aspects of pure and applied logic taught by international and Australian experts. The school provides a unique learning experience for all participants, backed up with state-of-the-art computational science facilities at the ANU.

    The school is most suitable for


    Registration: Closes Friday, 1 November 2002. Registrations after this date will attract a 20 percent surcharge.

    Visit the Web site for more information. To discuss this invitation in more detail, including advice on suitable candidacy, please contact John Slaney at the Automated Reasoning Group:

    Email lss-admin@arp.anu.edu.au; phone +61 2 6125 8630; fax +61 2 6125 8651

    Gail Pieper 2002-09-11