No. 37, September 1997

From the AAR President, Larry Wos...

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.

New Secretary for AAR

Maria Paola Bonacina
Dept. of Computer Science -- The University of Iowa
Iowa City, IA 52242-1419, U.S.A.

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.

Two New Books

The Efficiency of Theorem Proving Strategies

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.

Calls for Papers


An international workshop on First-Order Theorem Proving (FTP97) will be held at Schloss Hagenberg, near Linz (Austria), on October 27-28, 1997. The workshop will focus on first-order theorem proving as a core theme of automated deduction and will provide a forum for presenting recent work and research in progress.

Authors are invited to submit an extended abstract of up to five pages, by electronic mail to 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.


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 and contributions for the comparison in intuitionistic logic before November 1, 1997, to 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:


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 (

For further information, see the Web page.

Course on Theorem Proving Using Isabelle

A course entitled ``Introduction to Theorem Proving Using Isabelle'' will be given on September 9-11, 1997, at the University of Cambridge (Programme for Industry).

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 ( or see the Web site.

ACL2 Theorem Prover
Matt Kaufmann and J Moore

Version 1.9 of the ACL2 theorem-proving system has been released. ACL2 stands for ``A Computational Logic for Applicative Common Lisp.'' ACL2 is similar to the Boyer-Moore theorem prover, Nqthm, and Kaufmann's interactive extension, Pc-Nqthm. However, instead of supporting the ``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common Lisp. Furthermore, ACL2 is programmed almost entirely within that language. It is extensively documented in Postscript, HTML, and Emacs Info formats.

Download ACL2 Version 1.9 .

What's new .

AMS Mathematics Subject Classfication

We have received word that the American Mathematical Society has asked for comments about changes to the 1991 Mathematics Subject Classification (see the Web page). Several finite-model theorists have suggested that there be a new field called ``Logic in Computer Science" within area 68 of Computer Science and that it include a subfield devoted to finite-model theory. Interested persons are invited to send comments by e-mail to Jurek Tyszkiewicz ( so that a common proposal can be submitted to the AMS.

Erratum: Challenge Problems in First-Order Theories
Benjamin Shults

Abstract. This note contains an axiom missing from an article in AAR Newsletter No. 34.

Download PostScript or DVI.

On Quaife's Development of Class Theory
Johan G. F. Belinfante

Abstract. This brief note presents a list of corrections of misprints and other minor errors found in Chapter 2 and Appendix 2 of Art Quaife's book Automated Development of Fundamental Mathematical Theories.

PostScript or DVI.

Art Quaife

Abstract. Art Qaife adds here a few additional corrections for his book.

PostScript or DVI.

Replacing the Axioms for Connecting Lines
and Intersection Points by Two Single Axioms
Li Dafa

Abstract. The theorem prover ANDP is used to prove that 4 axioms of von Plato's axiomatization of constructive apartness geometry can be replaced by 2 axioms that avoid negations.

PostScript or DVI.

Is von Plato's Axiomatization Complete for Elementary Geometry?
Li Dafa

Abstract. This article discusses an intuitively valid statement in elementary geometry that should be included as a theorem of von Plato's apartness geometry.

PostScript or DVI.

Three Axioms of von Plato's Axiomatization
of Constructive Projective Geometry Are Not Independent
Li Dafa

Abstract. Experiments with the theorem prover ANDP indicate that three axioms in von Plato's axiomatization of constructive projective geometry are redundant.

PostScript or DVI.