NEWSLETTER

**Table of Contents**

Message from the AAR President

Call for Participation:
CADE-15

Workshop on Mechanization of Partial Functions

Workshop on Using AI Methods in Deduction

Workshop on Integration of Deduction Systems

Preliminary Call for Papers:
FTP'98

Can Model Builders Help Logicians in Building Infinite Models?

Book Announcements:

Automated Deduction - A Basis for Applications

Term Rewriting and All That

Ethics, Computing, and Medicine

**From the AAR President, Larry Wos...**

Our summer issue of the *AAR Newsletter*
features one of my favorite topics:
using an automated reasoning program
to assist the mathematician in solving difficult problems.
My thanks to N. Peltier for this
interesting article.

I hope AAR newsletter readers will also try the finite model generation exercise that Jian Zhang has provided.

Much of the rest of the newsletter is an invitation: you are invited--indeed, encouraged--to participate in CADE-15's lectures, workshops, and tutorials. As an added incentive, I note that Germany should be lovely at this time of year.

**CADE-15 Workshop on
Mechanization of Partial Functions**

**CADE-15 Workshop on Using AI Methods in Deduction**

**CADE-15 Workshop on Integration of Deduction Systems**

FTP'98, an international workshop on First-order Theorem Proving, will be held at Schloss Wilheminenberg, Vienna, Austria, on November 23-25, 1998.

FTP'98 is the second in a series of workshops intended to focus effort on first-order theorem proving as a core theme of automated deduction, and to provide a forum for presentation of very recent work and discussion of research in progress.

The workshop welcomes original contributions on theorem proving in classical, many-valued, and modal first-order logics, including resolution and tableau methods; equational reasoning and term-rewriting systems; constraint-based reasoning; unification algorithms for first-order theories; specialized decision procedures; propositional logic; abstraction; first-order constraints; complexity of theorem proving procedures; and applications of first-order theorem provers to problems in artificial intelligence, verification, mathematics, as well as other areas.

The technical program will include presentations of the accepted papers and invited talks. There will be ample time for questions and discussions in an informal atmosphere to foster the exchange of new ideas.

Authors are invited to submit an extended abstract of 5-8 pages. (See the FTP'98 home page www.logic.at/ftp98 for detailed instructions.) The submission deadline is August 31, 1998.

The extended abstracts that are accepted will be collected in a volume that will be distributed at the workshop. Additionally, the abstracts will be made available on the Web after the workshop. Authors of accepted abstracts will be invited to submit a full version, which will again be refereed. The selected papers will be published in the workshop proceedings; more details will become available soon.

Nicolas Peltier

Laboratory LEIBNIZ-IMAG

46, Avenue Félix Viallet 38031
Grenoble Cedex FRANCE

Nicolas.Peltier@imag.fr

**Summary:**
Since automated theorem
provers are becoming increasingly more powerful and easy to use, more and more
difficult problems---which
are interesting for mathematicians, logicians, or computer scientists---can
be solved by using theorem provers, often with some help of the
user (for choosing the inference rules, the strategy, etc.),
This is also true for model building: already fifteen years ago,
striking results were obtained with the help of theorem provers. Most of
these results concern finite mathematics, where
finite model builders were used to show the existence or nonexistence of
{\em finite} structures satisfying some properties.
In this work, we show how model-building methods can also be useful for
showing the existence of {\em infinite} structures. More precisely, we show
how to use an infinite model builder developed in our inference laboratory to
build a model for
a satisfiable formula introduced by Goldfarb in his proof of the
unsolvability of the G class with identity.

Jian Zhang

Email: zj@ox.ios.ac.cn

**Summary:**
In the mid-1980s, Allen and Hayes proposed axiomatizing temporal
intervals by using five axioms.
Galton later developed a three-element structure that satisfies the
first three axioms but falsifies the fifth.
This brief article shows how SEM was used
to generate one three-element model.

**Automated Deduction - A Basis for Applications**

Franz Baader and Tobias Nipkow have published a new book
*Term Rewriting and All That*
(Cambridge University Press, 1998; ISBN 0-521-45520-0).
As the back cover states,
this is the first English language textbook offering an
unified and self-contained introduction to the field of
term rewriting.

The book discusses all the basic material (abstract reduction systems, termination, confluence, completion, and combination problems), but also some important and closely connected subjects: universal algebra, unification theory, and Gröbner bases. Most of the material is presented in the functional language Standard ML (an appendix contains a quick and easy introduction to ML).

Intended as a textbook, *Term Rewriting and All That* contains
many examples and over 180 exercises.

The text is also an ideal reference book for professional researchers. It collects results reported in various conferences and journal articles in a unified notation, and gives detailed proofs of almost all the theorems. Each chapter also closes with a ``gentle guide'' to the literature.