ASSOCIATION FOR AUTOMATED REASONING

NEWSLETTER

No. 45, October 1999

Table of Contents

From the AAR President
Results of the CADE Trustee Elections
Calls for Papers

  • CADE-17
  • CAV 2000
  • CL 2000
  • FTP'2000
  • TANCS 2000
  • CSL 2000
    New Book

    From the AAR President, Larry Wos...

    This issue follows quickly on the last one, principally because we wished to announce the results of the CADE election of officers. We have also included calls for papers and demos, as well as an announcement of a contest for ATP systems.

    If the rate of progress in automated reasoning follows the pattern of the past decade, the next millenium should be most rewarding!

    Results of the CADE Trustee Elections

    Maria Paola Bonacina
    (Secretary of AAR and CADE)
    E-mail: bonacina@cs.uiowa.edu

    The 1999 CADE Trustee elections were held from September 17 through October 17. Ballots were sent by electronic mail to all members of AAR as of September 17, for a total of 396 ballots. Of these, 119 were returned with a vote, representing a participation level of 30%. The majority is 50% of the votes plus 1, hence 60.

    The following table reports the distribution of preferences:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    Harald Ganzinger 49 20 16 34 119
    Michael Kohlhase 24 25 19 51 119
    Neil V. Murray 21 15 15 68 119
    David A. Plaisted 25 47 8 39 119

    No candidate reaches a majority right away, and since Neil Murray turns out to be the weakest candidate by a few votes, his votes are redistributed, yielding the following new distribution:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    Harald Ganzinger 55 25 20 19 119
    Michael Kohlhase 31 27 33 28 119
    David A. Plaisted 31 45 31 12 119

    Again, no candidate reaches a majority, and Michael Kohlhase turns out to be the second weakest candidate, because the tie with David Plaisted in the count of the first preferences is broken by the difference in the second preferences. The redistribution of his votes yields the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    Harald Ganzinger 70 25 19 5 119
    David A. Plaisted 40 61 17 1 119

    At this point, Harald Ganzinger has a majority and is elected. His votes are redistributed, producing the following table:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    Michael Kohlhase 31 25 43 10 119
    Neil Murray 29 18 53 19 119
    David Plaisted 58 21 31 9 119

    None of the candidates has a majority to be elected, so that votes need to be redistributed again. The weakest candidate is again Neil Murray by a few votes, so that his votes are redistributed as follows:

    Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. Total
    Michael Kohlhase 45 40 29 5 119
    David Plaisted 67 35 13 4 119

    At this point, David Plaisted has a majority and is elected.

    On behalf of the AAR and CADE communities, congratulations to Harald and David on being elected, many thanks to Michael and Neil for running, and thanks to all those who voted.



    Calls for Papers

    CADE-17

    The 17th International Conference on Automated Deduction will take place June 17-20, 2000, in Pittsburgh, Pennsylvania. Original research papers (15 pages) are solicited in all aspects of automated theorem proving, automated reasoning, computer aided verification, formal methods, and static analysis. Systems descriptions (5 pages) are also solicited; system description submissions must include a URL for a Web page from which the system can either be run or obtained by reviewers. Both types of papers will be published in the proceedings of CADE-17 by Springer-Verlag. The deadline for submission is January 15, 2000.

    Proposals are also solicited for workshops (June 21) and tutorials (June 16). Anyone wishing to organize such an event should send (e-mail preferred) a proposal no longer than two pages to the workshop chair Michael Kohlhase (kohlhase@cs.uni-sb.de) by November 30, 1999. The proposal should describe the topic of the proposed workshop or tutorial and explain why the topic is relevant to CADE.

    Recent CADE workshops have included term schematizations and their applications, reasoning, automation of proofs by induction, empirical studies in logic algorithms, mechanization of partial functions, proof search in type-theoretic languages, automated model building, evaluation of automated theorem-proving systems, strategies in automated deduction, automated theorem proving in software engineering and in mathematics and integration of symbolic computation and deduction. Workshops may have the same topic as those of previous workshops, and this practice is encouraged.

    Recent CADE tutorials have included equality reasoning in semantic tableaux, proof systems for nonmonotonic logics, rewrite techniques in theorem proving, proof planning, parallelization of deduction strategies, resolution decision methods, constructive type theory, the use of semantics in Herbrand-based proof procedures, logical frameworks, theorem proving by the inverse method, deduction methods based on Boolean rings, higher-order equational logic, and term indexing in automated reasoning.

    For further information, see the Web site.

    CAV 2000

    The 12th Conference on Computer Aided Verification will take place in Chicago, Illinois, on July 15-19, 2000. The CAV 2000 conference is the twelfth in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation.

    The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. Topics include modeling and specification formalisms, algorithms and tools, verification techniques, applications and case studies, testing based on verification technology, and verification in practice.

    Submissions are solicited in two categories:

    The submission deadline for both types of paper is January 15, 2000.

    For further information, see the Web site.

    CL 2000

    The international conference on Computational Lagoic (CL 2000) will take place at Imperial College, London, UK, July 24-28, 2000. CL2000 is the first conference in a major new series of annual international conferences bringing together the various communities of researchers who have a common interest in computational logic. CL2000 is collocating with three conferences: DOOD2000: 6th Int'l Conference on Rules and Objects in Databases; ILP2000: 10th Int'l Workshop on Inductive Logic Programming; and LOPSTR2000: 10th Int'l Workshop on Logic-based Program Synthesis and Transformation.

    CL2000 will include seven streams covering various subfields of computational logic, each with its own separate program committee:

    The last three streams effectively constitute the former ICLP conference series that will be now integrated into CL2000. ILP2000 will be collocating as a separate conference.

    Papers on all aspects of the theory, implementation, and application of computational logic are invited. The deadline for submissions is February 1, 2000.

    For further information, see the Web site.

    FTP'2000

    FTP'2000 is the third in a series of workshops focusing on first-order theorem proving as a core theme of automated deduction and providing a forum for presentation of recent work and discussion of research in progress. The workshop will be held in conjunction with TABLEAUX 2000 at St Andrews, Scotland, on July 3-5, 2000.

    The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, and modal logics, including resolution, equational reasoning, term-rewriting, model construction, constraint reasoning, unification, propositional logic, specialized decision procedures; strategies and complexity of theorem-proving procedures; and implementation techniques and applications of first-order theorem provers to problems in verification, artificial intelligence, and mathematics.

    Authors are invited to submit papers in the following categories: (1) extended abstracts of 5-8 pages describing original results not published elsewhere, (2) position papers of 1-2 pages describing the author's research interests in the field, work in progress, and future directions of research, and (3) practical contributions of 1-5 pages consisting of new problem sets, system descriptions, or solution processes to problem sets. System demonstrations will be possible. Submission deadline for all papers is April 2, 2000.

    For further information, see the Web site.

    TANCS 2000

    The Tableaux Non-Classical Systems Comparison will take place at the 7th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) at St Andrews, Scotland, July 4-7, 2000.

    The TABLEAUX conferences are a major forum for the presentation of new research in all aspects of automated deduction. In order to stimulate automated theorem proving and satisfiability testing development in nonclassical logics, and to expose ATP systems to interested researchers, the TANC Systems Comparison will be held at TABLEAUX-00.

    The aim of TANCS is to compare the performance of fully automatic, non-classical ATP systems (based on tableaux, resolution, rewriting, etc.) in an experimental setting and promote the experimental study on theorem proving and satisfiability testing in non-classical logics. For TANCS-2000 the focus is on extended modal and description logics. In particular, benchmarks derived from combinatorial problems will be available for

    New benchmarks also will be available for converse propositional dynamic logic.

    Submissions are invited as original, unpublished experimental papers describing a theorem prover and its performance on the benchmarks of the TANCS 2000 Comparison. Beside the paper, entrants are requested to submit the executable (or source code) of their prover and a summary of the experimental data upon which their paper is based. The experimental papers, together with information on the comparison design and results, will appear in the proceedings of the TABLEAUX-2000 conference published by Springer Verlag in the LNAI series. The deadline for submission is January 19, 2000.

    The comparison of the submitted systems will be mainly based on two aspects: (1) effectiveness, measured by the type and number of problems solved, the average runtime for successful solutions the scaling of the prover as problems get bigger; and (2) usability, measured by the availability of the prover via Web or other sources the portability of the code to various platforms the ease of installation and use

    For further information, see the Web site.

    CSL 2000

    The annual conference of the European Association for Computer Science Logic will take place at Fischbachau/Munich, Germany, on August 21-26, 2000. The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. Topics of interest include automated deduction and interactive theorem proving, categorical logic and topological semantics, type theory, equational logic and term rewriting, higher-order logic, logic programming, constraints, modal and temporal logics, and program specification, transformation, and verification.

    Submitted papers (not to exceed 15 pages) must arrive by January 31, 2000. Papers accepted by the Program Committee must be presented at the conference and will appear in a proceedings volume, to be published by Springer-Verlag in the LNCS series.

    For further information, see the Web site.

    New Book

    A new book, entitled Handbook of Tableau Methods, edited by M. D'Agostino, D. M. Gabbay, R. Hahnle, and J. Posegga, has been published by Kluwer Academic Publishers, Dordrecht, 1999 (ISBN 0-7923-5627-6). The 670-page handbook presents a wide coverage of tableaux systems for various logics. If you would like to write a review of this handbook for possible publication in the Journal of Automated Reasoning, please contact Gail Pieper (pieper@mcs.anl.gov).

    Contents

    Introduction - M. Fitting
    Tableau Methods for Classical Proposaitional Logic - M. D'Agostino
    First-order Tableau Methods - R. Letz Equality and Other Theories - B. Beckert
    Tableaux for Intuitionsitic Logics - A. Waaler and L. Wallen
    Tableau Methods for Modal and Temporal Logics - R. Gore'
    Tableau Methods for Substructural Logics - M. D'Agostino, D. Gabbay, K. Broda
    Tableaux for Nonmonotonic Logics - N. Olivetti
    Tableaux for Many-Valued Logics - R. Hahnle
    Implementing Semantic Tableaux - J. Possegga and P. Schmitt
    A Bibliography on Analytic Tableaux Theorem Proving - G. Wrightson
    Index