No. 41 October 1998

Table of Contents
Message from the AAR President
Abstracts and Links to the CADE-15 Workshops
Call for Papers:

  • Tableaux'99
  • LICS 99
  • RTA 99
  • CADE-16
  • CAV'99
  • New Book
    Special Issue of the Journal of Automated Reasoning
    News from the AAR Secretary

    From the AAR President, Larry Wos...

    Kudos and comments: I am delighted at the excellent work of our secretary Maria Paola Bonacina in obtaining up-to-date e-mail addresses for our members. Please read her article to learn about changes in the AAR membership and how these changes may affect you.

    As she notes, we view the AAR newsletter as a mechanism for scientific exchange. We want your contributions: do you have an open question, an exercise in automated deduction that you have found useful with students, a new reasoning program? Or do you have a problem you would like to have solved? (I especially enjoy trying to find shorter proofs for challenging problems.) Please send these to our newsletter editor Gail Pieper (

    Abstracts and Links to the CADE-15 Workshops

    Many of you were at the CADE-15 conference in Lindau, Germany, and had the opportunity to attend the various workshops offered. For those who wish more information about those workshops, we give here the links to the appropriate Web sites.

    Problem-Solving Methodologies with Automated Deduction

    Using AI Methods in Deduction

    Proof Search in Type-Theoretic Languages

    Strategies in Automated Deduction

    Integration of Deduction Systems

    Automation of Proof by Mathematical Induction

    Mechanization of Partial Functions

    Call for Papers


    Tableaux'99, an international conference on analytic tableaux and related methods, will take place on June 8-11, 1999, at Saratoga Springs, New York.

    Tableau methods have been found to be a convenient formalism for automating deduction in various nonstandard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis. The conference brings together researchers interested in all aspects-theoretical foundations, implementation techniques, systems development and applications-of the mechanization of reasoning with tableaux and related methods.

    The conference will include contributed papers, tutorials, system descriptions, a poster session, and invited lectures. A special feature will be a comparison of theorem provers. This comparison is organized by Fabio Massacci of Universita di Roma ``La Sapienza". For information, send e-mail to

    Topics of interest include the following:

    Submissions are invited in three categories: (A) Original research papers (up to 15 pages), (B) Original papers on system descriptions (up to 5 pages), and (C) Tutorials in all areas of analytic tableaux and related methods from academic research to applications (proposals up to 5 pages). The conference proceedings (including accepted papers of categories A and B) will be published within the LNAI series of Springer. Tutorial submissions (category C) may be at introductory, intermediate, or advanced levels. Novel topics and topics of broad interest are preferred. Authors are requested to submit via email in PostScript to the Program Chair Neil V. Murray ( by December 4, 1998. Additional information is available through WWW address: nvm/tab99/.


    The second Federated Logic Conference (FLOC'99) will be held in Trento, Italy, in July 1999. Four conferences will participate in FLoC: Conference on Automated Deduction (CADE), Conference on Computer-Aided Verification (CAV), IEEE Symposium on Logic in Computer Science (LICS), and Conference on Rewriting Techniques and Applications (RTA).

    LICS 99

    The Fourteenth Annual IEEE Symposium on Logic in Computer Science will take place on July 2-5, 1999, in Trento, Italy. The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense. Topics of interest include abstract data types, automated deduction, bounded arithmetic, categorical models and logics, combination of logics, concurrency, constraint programming, constructive mathematics, database theory, denotational semantics, domain theory and applications, finite model theory, formal methods, game semantics, hybrid systems, logics of knowledge, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logics of programs, logic programming, modal and temporal logics, model checking, logical aspects of protocol security, rewriting, semantics, software specification, type theory and type systems, universal algebra, and verification. Authors should send an extended abstract to the program chair,, and to the associate chair,, by December 10, 1998.

    Of special interest is the Kleene Award for Best Student Paper, an award of $500to be given for the best student paper, as judged by the program committee.

    For more information, see

    RTA 99

    The Tenth International Conference on Rewriting Techniques and Applications will take place July 2-4, 1999, in Trento, Italy, as part of the Federated Logic Conference FLoC'99 (

    Papers are solicited in any of the following or related areas:

    In addition to full research papers (15 pages), descriptions of new working systems (4 proceedings pages) and problem sets that provide realistic, interesting challenges in the field of rewriting techniques are also welcome. High-quality papers on new applications of rewriting techniques are particularly encouraged. Submissions must reach the program chairmen by December 1, 1998. The conference proceedings will be published by Springer-Verlag as part of their Lecture Notes in Computer Science series.

    For further information, see


    CADE is the major forum for presentation of research in all aspects of automated deduction. CADE-16 will take place July 7--10, 1999, in Trento, Italy, as part of FLoC'99. Original research papers and descriptions of working automated deduction systems are solicited.

    Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, nonstandard, and meta-logics, and type theory. Methods of interest include saturation, tableaux, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, logical frameworks, and A I-related methods for deductive systems such as proof planning and proof presentation. Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer ma thematics, and deduction for natural language processing and other AI areas. Special topics of interest include proof theory, human-computer interfaces, distributed deduction, and search and simplification heuristics. Research papers can be up to 15 proceedings pages, and system descriptions can b e up to 4 pages. The proceedings of CADE-16 will be published by Springer-Verlag in the LNAI series. Papers should be compressed, then uuencoded, then e-mailed to the program chair Harald Ganzinger, Max-Planck-Institut für Informatik, Im Stadtwald, 66123 Saarbrücken, Germany; Phone: +49 681 9325 201; FAX: +49 681 9325 299; E-mail: All submissions must be received by January 5, 1999. Details on the procedure and alternatives can be found at the CADE-16 Web site


    CAV'99 is the eleventh in a series dedicated to the advancement of the theory an d practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applicat ions, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The topics of interest include modeling and specification formalisms, algorithms and tools, (such as model checking, synthesis, and automated deduction), verification techniques, applications and case studies, and testing based on verification technology. Authors must submit papers by January 3, 1999. The proceedings of the conference will be published in the Springer-Verlag Lectu re Notes in Computer Science series. Please direct all inquiries about CAV'99 to cav'

    New Book

    A new book Theorem Proving with the Real Numbers, by John Harrison, has been published by Springer-Verlag. The book may appeal to people interested in the formalization of mathematics, computer-aided verification, and related fields.

    The following summary is taken from the publisher's Web page at The book can be ordered directly from there.

    Theorem Proving with the Real Numbers discusses the formal development of classical mathematics using a computer. It combines traditional lines of research in theorem proving and computer algebra and shows the usefulness of real numbers in verification. This book aims to show that a theory of real numbers is useful in practice as well as theoretically interesting, and that the `LCF' style of theorem proving is well suited to the kind of work described.

    CONTENTS: Introduction - Constructing the Real Numbers - Formalized Analysis - Explicit Calculations - A Decision Procedure for Real Algebra - Computer Algebra Systems - Floating Point Verification - Conclusions - Logical Foundations of HOL - Recent Developments - Bibliography - Index

    200 pages
    234 x hardcover

    Some of the theories described are distributed in the examples directory of the HOL Light prover, available via the Web page

    Those persons interested in obtaining the rest of the HOL code should contact the author:

    Call for Papers:
    Special Issue of the Journal of Automated Reasoning

    SAT 2000
    (satisfiability at the start of the year 2000)
    Guest Editors:
    Ian P. Gent and Toby Walsh
    University of Strathclyde

    In the 1990s, there has been an explosion of research into propositional satisfiability (or SAT). There are many factors behind the increased interest in this area. One factor is the improvement of search procedures for SAT. New local search procedures like GSAT and WalkSAT are able to solve SAT problems with thousands of variables. At the same time, implementations of complete search algorithms like Davis-Putnam have been able to solve open mathematical problems. Another factor is the identification of hard SAT problems at a phase transition in solubility. A third factor is the demonstration that we can often solve real world problems by encoding them into SAT. The 1990s have also seen an improved theoretical understanding of SAT, particularly in the analysis of phase transition behaviour. In light of this, there will be a special issue of the Journal of Automated Reasoning, SAT 2000, on the state of the art for research into satisfiability as we move into the year 2000.


    We will consider empirical, theoretical or application oriented papers about SAT. Possible topics include (but are not limited to) the following:





    Prospective contributors are warmly invited to contact either, or both, of the guest editors to discuss the suitability of topics and papers. We especially welcome papers that discuss practical applications. In addition to presenting new research, all papers should provide a brief summary of their area so that outsiders can have an overview of the state of research into SAT at the start of the new millennium.


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

    Dr. Ian Gent
    Department of Computer Science
    University of Strathclyde
    Glasgow G1 1XH
    Phone: +44 141 548 4527
    Fax: +44 141 552 5330


    To ensure topicality of the special issue, submissions, reviewing and revision of papers will be held to very fixed and tight deadlines.

    To help us achieve this tight timetable, we have approached eminent researchers to form a review panel, although final decisions on papers will rest with the guest editors in collaboration with the editor of JAR. We will also expect authors of submitted papers to help with reviewing to this timetable.

    Review Panel

    News from the AAR Secretary

    Maria Paola Bonacina
    Dept. of Computer Science - The University of Iowa

    I have been the secretary of the Association for Automated Reasoning for one year, and the time has come to update everyone on the state of the association. As of September 30, 1998, the association counts 291 members, all of whom have a valid e-mail address. One year ago we had 338 members, but only 277 valid e-mail addresses, which means part of my work this year has been to reorganize the records, making sure that the newsletter reaches as many people as possible and pruning obsolete data. I am happy to welcome 42 new members who enrolled during 1998 for the first time, and because many of them joined by registering to CADE-15, many thanks go to Wolfgang Bibel and the CADE-15 organizing committee for the excellent work done in Lindau.

    Now that our basic records have been put in order, I would like to extend them by collecting the URL's of the home pages of members on the Web. This is done on a purely voluntary basis: if members wish to include their URL's in their AAR records, they can send them to me at

    On another side, I have been looking into augmenting the scientific contents of the AAR newsletter. For this purpose, I proposed to include in the newsletter the Web pages of the CADE workshops. By following the links in this issue, readers can access all papers, abstracts, and position papers that were presented at the CADE-15 workshops in Lindau. Many thanks go to the workshop organizers for making this possible by maintaining the Web pages. I also would like to encourage all members to send contributions, and help us make our newsletter a primary vehicle for the rapid diffusion of scientific communications in our field.

    Based on the consideration that the publication of the newsletter on the World Wide Web has annulled all postage costs for the association, the AAR officers (President Larry Wos, Vice-President Hans-Jurgen Ohlbach, Treasurer Larry Henschen and I) agreed that the AAR will no longer collect dues from its members. New members enroll by sending their data to the secretary, while existing members are kindly requested to confirm their membership annually, also by e-mail to the secretary. All members have the responsibility of keeping their data with the association up to date, informing the secretary of address or affiliation changes by e-mail. Similarly, members should inform the secretary by e-mail if they wish to leave the association.

    Since September marks in many ways the beginning of a new year (at least in academia), I would like to conclude with best wishes for another year of good work and achievement in automated reasoning.

    Next: About this document
    Wed Sep 30 20:42:07 CDT 1998