NEWSLETTER
Welcome to our first Web-based AAR newsletter (also available by e-mail). We present several articles by one of our regular contributors, Li Dafa. He has been exploring various aspects of Jan von Plato's axiomatization of constructive apartness geometry and has some interesting new conclusions. For your fall reading, I also include notices about two new books. The first, by D. Plaisted and Y. Zhu, focuses on one of my favorite topics -- strategy. The second book is a marvelous collection of essays, entitled Automated Reasoning and Its Applications, that Bob Veroff has put together.
News: I am pleased to announce that Maria Paola Bonacina has agreed to be our new secretary (see her article immediately following). Dues for AAR membership (which still includes a substantial discount to the Journal of Automated Reasoning) should be sent to her at the Department of Computer Science, The University of Iowa, Iowa City, Iowa 52242-1419. I deeply thank Bob Veroff for his long service as AAR secretary.
I have been happy to accept Larry's invitation to become the new secretary of the Association for Automated Reasoning. I thank Larry for his offer and Bob Veroff for his work as the previous secretary of AAR. Bob and Gail Pieper have been very helpful in this transition time, when the change of secretary overlapped with the move to the new form of distribution of the newsletter via the World Wide Web.
As of September 25, 1997, the association counts 338 members, but only 220 are current (i.e., the dues expire in 1997 or later). The notification message that the newsletter is published on the Web is sent to all members whose e-mail address is known (277 people). This message reports the date when the membership expires. All members are kindly invited to take note and pay their dues if they wish to remain members. The dues are $7 for one year, $13 for two years, or $18 for three years, and instructions for payment are posted on the AAR Web page maintained by Bill McCune.
The World Wide Web is now the primary way of diffusion of our newsletter. Those members who have difficulty with this can contact me by e-mail or post for alternative solutions. Also, if a member has recently moved, or has reason to believe that his records with the Association may not be current, he is invited to send me the data, and especially the correct e-mail address.
I am looking forward to a time of growth and excitement in the automated reasoning community, and I thank all for their cooperation.
The book The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis by David A. Plaisted and Yunshan Zhu introduces mathematical techniques for the analysis of the efficiencies of theorem-proving strategies. In particular, it develops techniques that permit one to estimate the sizes of the search spaces generated by theorem provers on various propositional and first-order problems. Such an analysis helps to supplement empirical observations obtained by running provers on examples. The book also gives insight into the comparative advantages of various strategies, as well as suggesting new directions for research.
This book is aimed at students and researchers working in the fields of automated deduction, mathematical logic, artificial intelligence, and computational complexity. It may be ordered from the following address: Informatica International, Inc., Department Vieweg, 275 C Marcus Blvd., Hauppage, New York 11788; Phone (516) 952-1676; Fax (516) 952-1685.
Automated Reasoning and Its Applications
MIT Press has published a new book Automated Reasoning and Its Applications: Essays in Honor of Larry Wos edited by Robert Veroff with Gail W. Pieper (ISBN 0-262-22055-5). The book comprises nine original articles by the world's leading researchers in automated reasoning. Included is an informal history of the ``culture'' of automated reasoning at Argonne; articles on automated reasoning theory, applications, and systems; and a discussion of metalevel reasoning as the next step toward more advanced automated reasoning systems. For a list of the book contents and for ordering information, see the Web site.
Authors are invited to submit an extended abstract of up to five pages, by electronic mail to ftp97@cs.uiowa.edu. See the Web site for instructions. The submission deadline is August 27, 1997. Accepted abstracts will be collected in a technical report distributed at the workshop. A special issue of the Journal of Symbolic Computation is planned.
The technical program will include presentations of the accepted papers and an invited talk by Bruno Buchberger (RISC) on the Theorema Project. Ample time will be provided for questions and discussions in an informal atmosphere to foster the exchange of new ideas.
The workshop is to be held right before CP97, the International Conference on
Constraint Programming,
with postconference workshops on November 1.
Attendance at both conferences is encouraged.
Tableaux'98
An international conference on Analytic Tableaux and Related Methods
will take place at the
Conference Centre Boschoord, Oisterwijk (near Tilburg),
the Netherlands, May 5-8, 1998.
The objective is to bring together researchers interested in all aspects of the mechanization of reasoning with tableaux and related methods (e.g., sequent calculi, connection method) and working on theoretical foundations, implementation techniques, systems development, and applications. One or more tutorials will be part of the conference program.
The Tableaux'98 conference will feature a comparison of theorem provers for intuitionistic and modal propositional logics. This comparison is organized by Alain Heuerding and Roy Dyckhoff. Contributions for the comparison in modal logics should be submitted before November 1, 1997, to heuerd@iam.unibe.ch and contributions for the comparison in intuitionistic logic before November 1, 1997, to rd@dcs.st-and.ac.uk For further information, see the Web site.
Submissions are
invited in three categories:
(1) original research papers (up to 15 pages);
(2) system descriptions (up to 5 pages);
and
(3) tutorials
(proposals up to 5 pages).
The conference proceedings, consisting of the accepted papers of categories 1
and 2, will be published within the LNAI series of Springer.
Papers or proposals for
tutorials should be submitted by e-mail, in the form of Postscript files,
to the Program Chair before November 15, 1997:
H.C.M.deSwart@kub.nl.
KR'98
The Sixth International Conference on Principles of
Knowledge Representation and Reasoning
will take place in
Trento, Italy, on June 2-5, 1998
(with workshops and coordinated events May 30 - June 1).
KR'98 is intended to be a place for the exchange of news, issues, and results among the community of researchers in the principles and practices of knowledge representation and reasoning (KR&R) systems. The organizers encourage papers that present substantial new results in the principles of KR&R systems while clearly showing the applicability of those results to implemented or implementable AI systems. Also encouraged are ``reports from the field'' of applications, experiments, developments, and tests. Initial submissions (of at most twelve pages) should be received by December 1, 1997.
A number of workshops and adjoining meetings will be held in conjunction with KR'98. Anyone interested in organizing such a meeting should contact the workshops coordination chair Lin Padgham (linpa@cs.rmit.edu.au).
For further information, see the Web page.
Theorem-proving systems are growing in popularity and are demonstrating their utility in many fields: hardware/software verification, program synthesis, artificial intelligence, and mathematics. The course (taught by Dr. Lawrence Paulson, the originator of Isabelle) will introduce participants to the Isabelle system, developed at Cambridge University and used in many research establishments. A typical application of Isabelle is to prove the correctness of cryptographic protocols.
Isabelle has built-in support for several logics, including first-order logic (FOL), higher-order logic (HOL), Zermelo-Fraenkel set theory (ZF) and extensional constructive type theory (CTT). New logics can also be introduced by specifying their abstract syntax, notation, and inference rules. This feature makes Isabelle uniquely flexible and applicable to many domains.
The course is highly practical, with numerous hands-on sessions. The lectures and terminal sessions will enable participants to perform their own Isabelle proofs in higher-order logic.
The course is intended for both academic and industrial researchers in the fields of computer science and logic. Participants must have experience with X workstation environments and should also be familiar with elementary logic. Experience with a functional programming language such as ML would be helpful, though not essential.
For information or a registration form, please contact Claire Derbyshire (ccd21@cus.cam.ac.uk) or see the Web site.
Download PostScript or DVI.
PostScript or DVI.
PostScript or DVI.
PostScript or DVI.
PostScript or DVI.
PostScript or DVI.