\documentstyle[11pt]{article}
\def\Goedel{G\"{o}del}

\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}


\setlength{\oddsidemargin}{-0.2in}
\setlength{\evensidemargin}{0.2in}
\setlength{\topmargin}{-1mm}
\setlength{\topskip}{0in}
\setlength{\headsep}{0in}

\setlength{\textwidth}{6.4in}
\setlength{\textheight}{8.9in}
\renewcommand{\baselinestretch}{1.1}
\setlength{\parskip}{1.5mm}

\hoffset=.25in
\def\parno{\par\noindent}

\let \imp = \Rightarrow



\newcommand{\Grobner}{Gr\"{o}bner}
\newcommand{\RRL}{{\sl RRL}\ }
\newcommand{\ERRL}{{\sl RRL}}
\newcommand{\rewrite}{\rightarrow}
\newcommand{\IF}{{\bf~if~}}
\newcommand{\OR}{\vee}
\newcommand{\AND}{\wedge}

\begin{document}


\begin{center}
{\LARGE {\Huge A}SSOCIATION \hspace{.05in} FOR \hspace{.05in} {\Huge A}UTOMATED
\hspace{.05in} {\Huge R}EASONING \\[.2in]
NEWSLETTER}\\[.1in]
{\Large No. 35 \hspace{4.1in} December 1996}\\
\rule{6.3in}{.02in}
\end{center}

\vspace{.3in}
\noindent
{\large \bf From the AAR President, Larry Wos...}

This issue of the {\it AAR Newsletter} was completed in 1996 but, because Argonne closes for two weeks in December, did not get
printed until January.
So, it's a grand way to end the old year---with McCune's solution to the long-standing
Robbins problem.
And it's a grand way to start the new year---with a new challenge competition for automated
reasoning programs and with several new
books for eager reviewers.

Since the Robbins problem has now been settled,
do any of you or your colleagues have open questions to take its place---questions
that appear to be amenable to attack with an automated reasoning program? 

\vspace{.2in}

\begin{center}

{\Large \bf Robbins Algebras Are Boolean}\\[1ex]
William McCune (mccune@mcs.anl.gov)
\end{center}

The Robbins problem---are all Robbins algebras Boolean?---has been solved:
Every Robbins algebra is Boolean. This theorem was proved automatically by
EQP, a theorem-proving program developed at Argonne National Laboratory.

\section*{The Problem}

In 1933, E. V. Huntington presented [1,2] the following basis for Boolean
algebra:
\begin{tabbing}
00000000\=\kill
\>    $x + y = y + x$.                    \`  [commutativity]\\
\>    $(x + y) + z = x + (y + z)$.        \`  [associativity]\\
\>    $n(n(x) + y) + n(n(x) + n(y)) = x$. \`  [Huntington equation]
\end{tabbing}
At that time, Herbert Robbins conjectured that the
Huntington equation can be replaced with a simpler one [5]:
\begin{tabbing}
00000000\=\kill
\>    $n(n(x + y) + n(x + n(y))) = x$.   \`   [Robbins equation]\\
\end{tabbing}
Robbins and Huntington could not find a proof, and the problem was later
studied by Tarski and his students [6], but no proof was found.

Algebras satisfying commutativity, associativity, and the Robbins equation
became known as Robbins algebras. It is clear that every Boolean algebra is
a Robbins algebra, so the interesting problem was whether every Robbins
algebra is Boolean. In other words, can the Huntington equation be derived
from commutativity, associativity, and the Robbins equation?

In 1979, S. Winker learned of the problem from his advisor, J. Berman. L. Wos
suggested attacking the problem by studying Boolean conditions
that might make a Robbins algebra Boolean. 
Many such conditions were found.
Several, such as idempotence and existence of a zero, 
were easily shown by Argonne's theorem provers to make a Robbins algebra
Boolean. Winker then showed [3,4] that each of the conditions
\begin{tabbing}
00000000\=\kill
\>    $\exists C \exists D, C+D=C$       \`  [first Winker condition]\\
\>    $\exists C \exists D, n(C+D)=n(C)$ \`  [second Winker condition]\\
\end{tabbing}
also suffices, with proofs by hand using insight from theorem prover
searches.  (In 1992 and 1996, respectively, the two Winker conditions were
shown automatically to be sufficient [7].)

\section*{The Solution}

The proof that solves the Robbins problem was found October 10, 1996, by the
theorem prover EQP [7]. EQP is similar in many ways to our more well known
program Otter. The main differences are that EQP has associative-commutative
(AC) unification, is restricted to equational logic, and offers more
paramodulation strategies.

EQP proved that every Robbins algebra satisfies the second Winker condition,
by refuting (with built in AC unification) the set
\begin{tabbing}
00000000\=\kill
\>    $n(n(n(y)+x)+n(x+y)) = x$. \`  [Robbins equation]\\
\>    $n(x+y) \neq n(x)$.          \`  [denial of second Winker condition]\\
\end{tabbing}
It follows immediately from this and the Winker lemma that all Robbins
algebras are Boolean.

The successful search took about eight days on a UNIX machine and used
about 30 megabytes of memory.  Subsequent searches have derived the
Huntington equation; that is, the automatic proof no longer
relies on the Winker lemmas.

See http://www.mcs.anl.gov/home/mccune/ar/robbins/ for more information,
including the proofs.

\section*{References}

\noindent
1. E. V. Huntington, ``New sets of independent postulates for the algebra
of logic'', {\it Trans. AMS} 35, 274--304 (1933).

\noindent
2. E. V. Huntington, ``Boolean algebra: A correction'', {\it Trans. AMS} 35,
557--558 (1933).

\noindent
3. S. Winker, ``Robbins algebra: Conditions that make a near-Boolean
algebra Boolean'', {\it J. Automated Reasoning} 6(4), 465--489 (1990).

\noindent
4. S. Winker, ``Absorption and idempotency criteria for a problem in
near-Boolean algebras'', {\it J. Algebra} 153(2), 414--423 (1992).

\noindent
5. H. Robbins, Telephone conversation, October 15, 1996.

\noindent
6. L. Henkin, J. D. Monk, and A. Tarski, {\it Cylindric Algebras, Part I,}
North-Holland, 1971.

\noindent
7. W. McCune, ``33 basic test problems: A practical evaluation of
some paramodulation strategies'',  preprint ANL/MCS-P618-1096,
Argonne National Laboratory, 1996.


\vspace{.2in}


%From walther@inferenzsysteme.informatik.th-darmstadt.de Tue Nov 19 10:25:05 1996
\begin{center}
{\Large \bf Automated Deduction as an International Discipline -- \\
An open letter to the president of CADE}\\ [1ex]
Pierre Lescanne (Nancy, France) and  Christoph Walther (Darmstadt, Germany)
\end{center}
  
  
During this year's Conference on Automated Deduction (July 30 - August 3, Rutgers University, N.J.), new democratic bylaws were
adopted that give the membership more rights in the administration of
CADE than the bylaws that were established when CADE was
incorporated some years ago in the state of Illinois. However, as a
result of the former election process, the current board of trustees is
U.S. dominated and does not reflect the activities in automated
deduction throughout the world: It consists of 1 trustee from the UK,
1 trustee from Australia, and 5 trustees from the U.S. reasoning
community. This is surprising, at least if one considers the development
of the field in the past decade, which is illustrated by the following table
showing the contributions to the last five CADEs in percentage:

\begin{tabular}{lllll}
Year    &     U.S.      &     EU      &    Other     &    Site \\ \hline
1988    &    61 \%     &    35 \%     &     4 \%      &   Argonne, Ill.\\
1990    &    51 \%     &   45 \%     &     4 \%      &   Kaiserslautern, Germany \\
1992    &    44 \%     &    49 \%     &     7 \%      &   Saratoga Springs,  N.Y.\\
1994    &    23 \%     &    73 \%     &     4 \%      &   Nancy,  France\\
1996    &    19 \%     &    79 \%     &     2 \%      &   New Brunswick, N.J.\\
\end{tabular}

        We doubt that the policy of CADE's trustees, to let the largest
reasoning community play only a minor role in the administration of
CADE, would be beneficial for CADE's future. We also believe that it
seems not wise to dispense with almost all of the experiences, knowledge,
and skill of one successful part of the reasoning community for the
administration of CADE. Proceeding in such a way risks the danger of
splitting the community into two parts such that Europe eventually
organizes its own event (which then would weaken the whole reasoning
community).

        Another issue is the choice of program chairs: 4 PC chairs from the
U.S., 1 from Australia, but only 1 from Europe have been selected since
CADE-9 in 1988. Remembering the developments of the past
decade, it is hard to believe that there is no one in Europe who is ready,
willing, and able to do the job. This is not a question of the qualification
or the reputation of the selected chairs, but the question of why a
successful part of the reasoning community is withheld from this
position. We think that it is time to change this disposition and to choose
the future chairs according to the real picture of the community.

        The problem resulting from the domination by one community was
visible during the business meeting, which required a thorough
background in the American culture of standing orders and rules to
come to a democratic decision, which made it difficult for many from
other parts of the world to follow and to contribute to the procedure.
The problem of domination also became obvious at the panel session
entitled ``Does Automated Deduction Have a Future?" There was only
one panelist from Europe, and the other five panelists from the U.S. soon
focused on the funding problems of the U.S. community. This caused
some trouble and resistance from the floor because many felt that the
future of the field also outside the U.S. would be worth discussing. There
are communities also in Europe that are successful, and it is pure
ignorance to dispense with the experiences gathered in other cultures
with other traditions, other systems of education, and other ways of
funding research. The attendance of this year's CADE would have
allowed to set up a panel for discussing the future of the field in all
aspects trying to find answers helpful for the whole community.

        For all these reasons we urge for a change in the administration of
CADE: Instead of running CADE in a way which was reasonable and
beneficial 15 or 20 years ago, the trustees should give the European
reasoning community an appropriate voice wrt. the board of trustees,
the selection of program chairs, and the composition of panels. This
would yield an optimal identification of the members of the community
with CADE, it would be beneficial for CADE's future and for further
developing automated deduction as a real international discipline.








\vspace{.2in}
\begin{center}
{\Large \bf Response to the Open Letter}\\ [1ex]
Mark Stickel, President of Trustees, CADE, Inc.
\end{center}

Although most CADE trustees and recent program chairs are American, this
is a transitory phenomenon (two Americans, Loveland and I, will leave
the board of trustees next year; the 1998 program chair, probably
European, will become a trustee when appointed; two trustees will be
elected at CADE in 1997).  Moreover, the nationality of the trustees is
only one indicator of the internationalism of CADE.  For example, note
that CADE will be held outside the United States at least the next three
times---in Australia in 1997, in Germany in 1998, in Italy in 1999 (there
has been no discussion yet about locations after 1999).  The program
committee for CADE in 1997 is mostly non-American (22 out of 32).  The
program chair for CADE in 1998 has not been selected yet, and the
current program committee is being consulted before a selection is made,
but it is the trustees' wish to select a European program chair for 1998
(there has been no discussion yet about program chairs after 1998).

The genesis and purpose of the inaptly named ``Does Automated Deduction
Have a Future?" panel at CADE were explained at that time.  Automated
deduction research is at risk in the United States, and the U.S. National
Science Foundation convened a meeting of U.S. researchers to discuss the
future of the field.  This panel was invited (not by the trustees, but
by the program chairs who have complete control over the conference they
chair) to report on what happened at that meeting and to seek input from
the whole CADE community to deal with the threat.  The opening
statements of panel members were limited to two minutes each so that
most of the time would be open discussion period for everyone attending.
Successes in Europe and problems in America should both be seen as
relevant to both groups.  Government research funding policies often
spread from one nation to another.

The business meeting at CADE was conducted as fairly and orderly as we
could.  Not being a native speaker of English was clearly a disadvantage
for participation.  I don't see any easy solution to this problem.  What
do you think would have helped?  I wonder whether the procedures at the
meeting acted to exclude non-American participation.  None of us were
experts on parliamentary rules, so there was no rigid adherence to such.
Are rules for proposing laws, amending them, and voting on them
substantially different in Germany and France than America?


\vspace{.2in}
\begin{center}
{\Large \bf The CADE-14 ATP System Competition\\ [1ex] 
Call for Participation}
\end{center}

The CADE conferences  are the major forum for the  presentation of new research 
in  all  aspects of  automated deduction.  In  order  to stimulate  ATP  system 
development, and to expose ATP systems to interested researchers, a competition 
for first-order ATP systems will be held at CADE-14, on Wednesday, July 16, 1997.

CASC-14 will evaluate the performance of sound fully automatic ATP systems. The
evaluation  will be in terms of the number of problems solved,  and the average
time taken for each successful solution; in the context of a specified CPU time
limit for  each solution  attempt,  and a bounded number  of eligible problems,
chosen  from the  TPTP Problem Library.  Information regarding  the competition
divisions,  problem selection and preparation,  time limits and timing,  system
execution,  performance evaluation,  special hardware demonstration  divisions,
and the conditions for participation can be found in the CASC-14 WWW pages:
\begin{verbatim}
    http://wwwjessen.informatik.tu-muenchen.de/~tptp/CASC-14/
\end{verbatim}

The competition  is being  organized by  Christian Suttner and Geoff Sutcliffe.
The  competition will be overseen by  a panel of knowledgeable  researchers who
are not  participating in the event.  It is planned  to publish the competition
results in a form that includes contributions written by entrants.

Registration  for  participation  closes  on May 15,  1997.  Please  fill in the
registration  form on the  WWW page  (or e-mail  one of the organizers).  Please
register as  early as possible  (e.g., right away),  so that the organizers can
ensure that sufficient resources are available.

\newpage
\noindent
{\bf CASC-14 Organizers:}

\begin{tabular}{ll}
    Christian Suttner    &             Geoff Sutcliffe\\
    Institut fuer Informatik   &       Department of Computer Science \\
    TU Muenchen      &                 James Cook University\\
    D-80290 Muenchen   &               Townsville, QLD 4811\\
    Germany          &                 Australia\\
    Tel [+49] 89 521098 &              [+61] 77 815085\\
    FAX [+49] 89 526502   &            [+61] 77 814029\\
    suttner@informatik.tu-muenchen.de &   geoff@cs.jcu.edu.au\\
\end{tabular}


\vspace{.2in}

%From dwl@cs.duke.edu Mon Dec 16 16:15:14 1996

\begin{center}
{\Large \bf 
Workshop on the Future Directions of Automated Deduction}\\ [1ex]
                      Donald Loveland
\end{center}


A workshop on the Future Directions of Automated Deduction 
was held in Chicago the weekend of April 20--21, 1996.
Participants were Peter Andrews, Wolfgang Bibel, Robert Boyer,
Shang-Ching Chou, Edmund Clarke, Robert Constable, Nachum Dershowitz,
Xiao-Shan Gao, Larry Henschen, Deepak Kapur, Ken Kunen,
Donald Loveland, Michael Lowry, Rusty Lusk, Bill McCune,
Ross Overbeek, Natarajan Shankar, Mark Stickel, Richard Waldinger,
Larry Wos, Hantao Zhang, and Xudong Zhao. The meeting was
organized by Donald Loveland, assisted by a Steering Committee
of Peter Andrews, Robert Boyer, Deepak Kapur, Mark Stickel, and 
Larry Wos.

The workshop was funded by the (U.S.) National Science Foundation,
which has considerable interest on the assessment of 
opportunities and future directions of our field. The NSF
has sponsored similar workshops in computer science recently
as part of an evaluation of allocation 
of research funds. The funds provided for the workshop 
permitted only a small number of attendees and only from
North America. (We were happy to be able to stretch the
funds to include Wolfgang Bibel to present the European
view of the status of automated deduction. As coordinator
for the major Schwerpunkt Deduktion program, 
Wolfgang was well suited to inform us of the 
European research in this area.)
We were eager to have users of automated deduction technology
included in the participants, but their inclusion limited us even more
in invitations to the active researchers in the field.
In spite of this consideration and that not all invitees could 
attend, we feel that we obtained good coverage of the major
areas of automated deduction.

To get input from
other centers of deduction research around the world, we 
issued a
Call for Contributions that would permit people to provide
electronic input to the topics we would address. These
documents were made available to all workshop participants 
prior to the workshop. We received a good number of high-quality 
contributions; they can be seen at the Web site
\begin{verbatim}
            http://www.cs.duke.edu/NSFwkshopAD/
\end{verbatim}

The meeting covered a day and a half, starting at 9 a.m.
Saturday and adjourning at noon Sunday. We wished 
discussion of the issues at hand to be the primary agenda,
so only two formal talks were scheduled: ``Opening 
Remarks: A Perspective for the Workshop''
by Dr. Kamal Abdali of the National Science Foundation
and ``European Efforts in Automated Deduction and Its
Applications'' by Wolfgang Bibel. The remainder of the
morning was dedicated to discussion of the contributions
received in response to our call. In the afternoon 
we split into working groups to provide more detailed
discussion by general area. The working groups were in 
the areas of mathematics, verification/specification,
symbolic computation, and AI/program synthesis/logic programming.
Later, small groups in education and in nonconventional
applications (such as formal methods in social science )
also convened. Late Saturday afternoon and Sunday 
morning were devoted to discussions by the the full
committee on the reports of the working subgroups.
Very informal discussions also occurred Saturday 
evening.

Clearly, it is important that the appropriate people in the
hierarchy at NSF have a good understanding of our achievements
and the opportunities that now exist.
We are taking care to present a report to NSF that best
accomplishes these goals. The report will reflect the
pragmatic attitude toward research now prevailing in the
United States but will still address the major basic research areas.
Research opportunities will be discussed within
the framework of the application areas of
verification/specification, program synthesis, mathematical
proof discovery, mathematics education, and
other applications. Topics as diverse as reasoning in
inductive domains and the integration of computer algebra
systems (and the need for soundness of such systems) occur
within this setting. We hope that those weighing the
worth of various research areas will see both the specific
utility of success in automated deduction and the 
tremendous intellectual accomplishment this would mean.

We intend to publish a
version of the report
in the near future.





\vspace{.2in}
\begin{center}
{\Large \bf Call for Book Reviewers}
\end{center}

We are seeking reviewers for the following books related to  automated reasoning
and automated deduction.
Those reviews approved by the book review editor,
Rick Stevens, will appear in the {\it Journal of Automated Reasoning.}

Currently, we have the following books available for review:

\begin{enumerate}

\item
{\it Automated Deduction in
Equational Logic and Cubic Curves,} by W. McCune and R. Padmanabhan,
Springer-Verlag, 1996

\item
{\it An Experimenter's Notebook with OTTER Tutorial,}
by Larry Wos, Academic Press, 1996

\item
{\it Extensions of First Order Logic,} by Maria Manzano, Cambridge University Press, 1996

\item
{\it For the Sake of the Argument: Ramsey Test Conditionals, Inductive Inference, and Nonmonotonic Reasoning,}
by Isaac Levi, Cambridge University Press, 1996

\item
{\it ML for the Working Programmer,} 2nd ed., by L. C. Paulson, Cambridge University Press, 1996
\end{enumerate}

Interested reviewers are asked to contact
Gail W. Pieper, pieper@mcs.anl.gov, for information
on the type of review we are seeking.


\vspace{.2in}

\begin{center}
{\Large \bf Call for Papers}
\end{center}

\noindent
{\bf HOA '97}

The 1997 workshop on Higher-Order Algebra, Logic and Term Rewriting 
will take place September 4--5, 1997, in Southampton, UK,
immediately following ALP '97 and PLILP '97.
The scope of the workshop includes higher-order aspects of
  algebra, logic, and model theory; term rewriting; specification and
  verification languages; computational logic and theorem proving;
  system implementations and case studies.
Extended abstracts (up to 4 pages) 
  should be sent to the program committee
  chairman:
Jan Heering, CWI, Kruislaan 413, 1098
  SJ Amsterdam, The Netherlands.
 E-mail: jan@cwi.nl. Fax +31 20 592
  4199.  URL http://www.cwi.nl/$\sim$jan/.
E-mail submissions are preferred.
The deadline for submissions is April 1, 1997.

\noindent
{\bf WoLLIC'97}

The Fourth
Workshop on Logic, Language, Information, and
Computation will take place in Fortaleza (Ceara'), Brazil,
on August 20--22, 1997.
Contributions are invited in the form of two-page (600
words) abstracts in all areas related to logic, language,
information and computation, including
 pure logical systems, proof theory, model theory, algebraic logic, type theory, category theory,
constructive mathematics, lambda and combinatorial calculi, program
logic and program semantics, nonclassical logics, nonmonotonic
logic, logic and language, discourse representation, logic and
artificial intelligence, automated deduction, foundations of logic
programming, logic and computation, and logic engineering.
Interested authors should submit an abstract,
preferably by e-mail to
wollic97@di.ufpe.br by June 1, 1997.
For further information, see http://www.lia.ufc.br/wollic97.


\vspace{.2in}
%From bshults@fireant.ma.utexas.edu Wed Dec  4 14:52:20 1996
{\begin{center}
{\Large \bf Erratum:  Challenge Problems in First-Order Theories}\\ [1ex]
Benjamin Price Shults,
The University of Texas at Austin
\end{center}

In the October 1996 {\it AAR Newsletter,}
I presented a number of challenge problems in first-order theories.
In the first example (about locally compact spaces)
the following corrections should be made:
\begin{enumerate}
\item
All
occurrences of continuous-from-to {\bf should be changed to}
continuous-from-onto.
\item
All occurrences of open-from-to
{\bf should be replaced with} open-from-onto. 
\end{enumerate}

These corrections do not change
any of the reasoning.
They do, however, make the knowledge base make more
  sense to people.

\end{document}
