%could add Turkey96
\documentstyle[11pt]{article}
\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. 33 \hspace{4.1in} June 1996}\\
\rule{6.3in}{.02in}
\end{center}

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

The debate continues. 
In this issue, we include the (recently modified) proposed CADE Bylaws and David Plaisted's  comments on this revised set.
I encourage AAR members to read the arguments presented 
 and
keep ever-present in mind that in most cases, like entropy, sharp change is
dangerous.


On a different note, G. Huang presents a solution to TopSpin.
For those researchers who enjoy puzzles---as I do---Huang's article will be of immediate interest.

Finally, for the curious, I cite the results of the recent survey
in the {\it AAR Newsletter:}
the overwhelming majority voted in favor of continuing paper
copy of the newsletter (I believe the tally was 3 to 1---{\it total}).

 
%bundy@aisb.ed.ac.uk
\vspace{.2in}
\begin{center}
{\large \bf Alan Robinson Receives the Herbrand Award}
\end{center}

 CADE, Inc., has announced that Alan Robinson will receive
the Herbrand Award at CADE-13.  The Herbrand Award is given by
CADE to honor a person or a group of people for exceptional
contributions to the field of automated deduction.  It carries a
certificate and a check for \$1000.  Previous awards have been
made at CADE-11 to Larry Wos and at CADE-12 to Woody Bledsoe.

Alan Robinson has generously asked for the \$1000 to be donated to
the Woody Bledsoe Student Travel Award, which will be used to
fund one or more students to attend CADE-13.


\vspace{.2in}
\begin{center}
{\large \bf CADE, Inc. Bylaws}\\
{\it Alan Bundy, President, CADE, Inc.}
\end{center}

	For those following the continuing saga of the CADE Inc.
bylaws, another installment is now available. The CADE Trustees
have produced a modified version of David Plaisted's proposed
amendments. These new proposals retain the essential elements of
David's proposals, namely, democratically elected Trustees, but change
some of the details that the Trustees were unhappy about. You can
view these proposed changes on the CADE web page on

	http://www.cs.albany.edu/$\sim$nvm/

In particular, there is a page that juxaposes the original
bylaws, David's amendments to them, and the trustees further
amendments, together with a commentary.

	There will be a vote on these proposed amendments at the
CADE Business Meeting during CADE-13. This will be held during
the evening of Wednesday, July 31, and not Saturday, August 3, as
it says in the advance programme.


\vspace{.2in}

%From plaisted@cs.unc.edu Sun Jun 23 17:49:06 1996


\begin{center}
{\large \bf The Trustees' Democratic Bylaws Proposal}\\
{\it David A. Plaisted}
\end{center}


	The trustees of CADE, Inc. recently proposed a democratic set
of bylaws for CADE.  Their proposed bylaws have some similarities to
those previously proposed by myself and some others.  In their
proposal, the trustees made some comments about our set of proposed
bylaws.  I would like to respond to these comments, as well as to
comment about the trustees' counterproposal.

	I commend the effort of the trustees to develop such a set of
bylaws, and also the fact that their proposal specifies three year
terms for trustees, as does our proposal (assuming that CADE meets
once a year).  However, their proposal has a number of deficiencies,
which the CADE community should be aware of.  I expect that the
trustees will modify their proposal, but this commentary is based of
necessity on their initial version.  In any event, these comments
should be of value in bringing relevant issues to light.

	There are a number of inessential differences between the
proposals which I will ignore.  One of the notable differences has to
do with the degree of democracy.  In the trustees' proposal, the
secretary, treasurer, and current and forthcoming program chairs are
automatic (that is, nonelected) trustees.  There will in addition be
six elected trustees.  Therefore it is conceivable that one-third (or
more) of the trustees could be nonelected.  This results in only a
partially democratic system.

	Another very serious problem with the trustees' proposal is
that motions passed at CADE business meetings are considered as only
advisory.  This means that the trustees can ignore them if they so
choose.  This results in a further weakening of the voice of the
membership in the governance of CADE.  I modified the wording of my
proposal to be more clear in specifying that motions passed at the
business meeting are binding on the trustees.

	In addition, the trustees' proposal specifies that amendments
to the constitution require a two-thirds majority.  This could mean
that the CADE community gets stuck with a set of bylaws that we find
out is not suitable, but no one can get rid of them because of the
two-thirds requirement.  My proposal specifies a simple majority,
which is more appropriate in an initial period until all the
implications of the bylaws are understood and experienced.

	Any of the above points is in itself sufficient reason to
reject the trustees' proposal.  There are also some other, less
serious problems with it.  The trustees propose that elections be
conducted according to a complicated single transferrable vote system.
This system has some advantages, but it is hard to understand, makes
it hard to count the votes, and makes it hard to verify that the votes
have been properly counted.  I proposed a two-round system.  Such
systems are well-tested, in common use, easy to understand and run,
and give voters a second chance to evaluate the candidates.  In
addition, in some ways my system is actually more sensitive to voter
preferences than the single transferrable vote system.

	The trustees' proposal also weakens the function of the
trustees as a nominating committee in giving the members a choice.  In
my system, the trustees will make at least three nominations in
addition to the current program chair and incumbent trustees, who are
automatic nominees (and not excluded from the slate as the trustees
stated).  The trustees' plan removes the automatic nominations and
only specifies that the trustees will nominate two individuals, who
are likely to be the current program chair and an incumbent trustee.

	Another issue slightly off the subject is that of verifying
the vote count when our proposal is voted on at CADE 13.  I requested
that some of the supporters of our proposal participate in the vote
count or at least be able to recount the ballots.  So far there has
been no response from the trustees, but I expect this to be
forthcoming.  I also requested that there be at most one proxy
controlled by one individual at CADE 13.

	In sum, the trustees' plan does have at least a partial
democratic aspect, and has short (three year) terms for trustees.  But
it also has a number of very serious drawbacks that make it
unacceptable in its current form.  I encourage the trustees to modify
their plan, which they may have done already by the time this issue
appears.  In contrast, the system proposed by myself and others is
more democratic and workable, and none of the criticisms raised
against it have any substance.  We believe that our proposal is more
worthy of your support.


\vspace{.2in}
\begin{center}
{\large \bf
 Using OTTER and Prolog to Solve TopSpin}\\
 {\it Guoxiang Huang}\\
Mathematics Department, University of Hawaii, Honolulu, HI 96822\\
      e-mail: huang\@math.hawaii.edu
\end{center}

%From huang@math.hawaii.edu Fri Apr 12 21:51:13 1996



%\input amstex
%\documentstyle {amsppt}
%\magnification=\magstep1
%\nologo
%\NoRunningHeads
%\NoBlackBoxes
%\pagewidth{6 truein}
%\pageheight{8.5 truein}
%\hcorrection{0.5 truein}
%\topmatter
%\title 
%\endtitle 
%\author Guoxiang Huang \endauthor
%\affil
%\endaffil
%\endtopmatter

%\document
%\baselineskip = 1.2\baselineskip

TopSpin consists of a circular track with 20 pieces numbered 1, 2, ...,
20 placed in the track, and a turnstile that  always holds 4 consecutive
pieces.
There are three legal
moves in TopSpin: slide all the pieces around the track one position in
the clockwise or counterclockwise directions, 
or flip the turnstile and its 4 pieces $180^{\circ}$. 
If we picture the turnstile at the top of the circular track, 
then sliding the pieces one position in either
direction corresponds to sliding the pieces 
through the turnstile one position to
the right or left. Thus we refer to the moves as {\it sliding left,
sliding right}, 
and {\it flipping}; and denote them as L, R, and F, respectively.

%\medpagebreak

\noindent
{\bf 1. The Representation}

Starting from the leftmost position of the turnstile, from left to right
we number the positions 1, 2, ..., 19, 20 in that order.
We use a 20-place relation $S$ to represent these 20 positions
and 20 constants 1, 2, 3, ..., 20 to name the 20 numbered
pieces. Thus a configuration of TopSpin is
represented by a literal $S(c_1, c_2, c_3, .., c_{20})$, where
$c_i\in\{1,2,3,...,20\}$. 
Corresponding to the three legal moves, we get the following three rules
for TopSpin:

$S(x_1,x_2,x_3,x_4 ..., x_{19},x_{20})\Rightarrow S(x_2,x_3,x_4,x_5,...,x_{20},x_1)$
    (move L)\par
$S(x_1,x_2,x_3,x_4,....,x_{19},x_{20})\Rightarrow S(x_{20},x_1,x_2,x_4,...,x_{18},x_{19})$ (move R)\par
$S(x_1,x_2,x_3,x_4,x_5,...,x_{19},x_{20})\Rightarrow  S(x_4,x_3,x_2,x_1,x_5,...,x_{19},x_{20})$
(move F).

%\medpagebreak

\newpage
\noindent
{\bf 2. Unscrambling the Pieces}

Given any initial board with scrambled pieces on the track, the problem
is to find a sequence of moves that unscrambles the pieces.
Using OTTER 3.0, we can always move
piece 20 to its destination first, then move piece 
19 to its destination, ...,
and finally we get a configuration:
$S(*,*,3,4,...,18,19,20)$ where $*,*$ is either $1,2$ or $2,1$.

But OTTER could not move $2$ to its destination when the $*,*$ is
$2,1$. In solving the subgoal of moving $5$ to its destination,
OTTER found a sequence of moves 
$${\it F L F R F L F R}$$ 
which permutes five consecutive pieces in 0.83 seconds
without moving the
remaining 15 pieces. This derived rule, written formally, is
 $$S(x,y,z,u,v,w_6, ..., w_{20})\Rightarrow  S(y,z,u,v,x,w_6,..., w_{20}).$$
Once we add this rule as a new axiom to the set of support, OTTER swaps
1 and 2 in 24 steps and in 252 seconds
while preserving the order of other pieces.

%\medpagebreak

\noindent
{\bf 3. Two Hard Problems}

One hard problem in TopSpin is turning the turnstile upside
down without changing the order of the pieces. The brochure that came
with the puzzle gave a 37-step solution.

To record the orientation of the turnstile, we add a 21st position to
the relations. The orientation position is 
filled with the constant `0' or `1' to 
indicate the two distinct orientations of the turnstile. 
The moves R and L do not change the value of the orientation position, 
but move F always changes the value.  

We found that the
following 31-step sequence of moves accomplishes the task of inverting the
turnstile with a minimal number of steps:  
$${\it R F L F R F L F L L F R R F L F R F R F L L F R F L L F R F R.}$$

Another hard problem is to find a minimal length of derivation
that switches two adjacent pieces while leaving the
other pieces fixed. The brochure that came with the puzzle gave a
49-step solution.  
We found the following 41-step sequence of moves that
accomplishes this task: 
 $${\it F L F R } 17 {\it (F L) L F R.}$$

We found both sequences and proved them to be minimal using Prolog and
OTTER. The search space is too large for OTTER to accomplish the tasks
alone. Working backward using OTTER, we generated all configurations
that were 12 steps from the goal. Then we used Prolog to search from
the initial board to these OTTER-generated configurations.
To constrain Prolog's depth-first search strategy, we added another place
in the relation to store the maximum search depth allowed. 
To show that the solutions were of minimal length, we let the Prolog
exhaustively search all possible shorter sequences. 
The second problem took about 23 hours on a 486 PC.





\end{document}


\vspace{.2in}
\begin{center}
{\large \bf
New Electronic Information}
\end{center}

\noindent
{\bf New Web Page in Mechanized Reasoning}

A new Web page  in mechanized reasoning is available. 
It consists of the information previously contained
in Carolyn Talcott's ``Mechanized Reasoning" page and Michael Kohlhase's
``Deduction Worldwide" pages and will replace these. To conserve existing
links and bandwidth it will be mirrored at both original sites:

\begin{flushleft}
  Europe: http://jswww.cs.uni-sb.de/ded/mr.html\\
  USA:    http://www-formal.stanford.edu/clt/ARS/ars-db.html
\end{flushleft}

The pages are still provisional.
The hope is that they will 
evolve to a WWW entry point to and a representation of all mechanized
reasioning activities.
Readers are invited to send in
interesting material, links, and
suggestions to
Michael Kohlhase,
kohlhase@cs.uni-sb.de,
http://jswww.cs.uni-sb.de/~kohlhase/, and to
Carolyn Talcott, 
clt@sail.stanford.edu,
http://www-formal.stanford.edu/clt/home.hmtl.


\noindent
{\bf New Software Verification E-Mail List}

Paul E. Black
(black@cs.byu.edu)
has created
a new software verification e-mail list
where people can
discuss issues related to proving programs.  To join the list, send
e-mail to majordomo@lal.cs.byu.edu.
The subject line does not matter.  The body must contain the line
``subscribe softverf''.
An automatic response should be sent within about an hour.

Black also intends to create World Wide Web pages with references and
resources related to software verification.

\end{document}


%\vspace{.2in}
%\begin{center}
{\large \bf Conferences}
\end{center}


\noindent
{\bf TPHOL96}



The 1996 International Conference on Theorem Proving in Higher Order Logics
will be held on August 27--30, 1996,
in Turku (Abo in Swedish)
in the southwest corner of Finland. Two tutorials are also included, starting
after midday on Monday, August 26.

The conference will be a venue for presentations on the following topics, among
others: advances in interactive theorem proving, proof automation and decision
procedures, applications of mechanized theorem proving, comparison between
different theorem proving approaches, exploiting external tools within theorem
provers and incorporating theorem provers into larger systems.
Tutorials and poster sessions will also be offered.

We note that
the third Workshop on Designing Correct Circuits (DCC) will be held from 
September 2--4, 1996, at Bastad in southern
Sweden. Thus, researchers outside Europe have an excellent opportunity
to attend both conferences.                                       

For further information, please contact the organizing committee
on ``orgcom@abo.fi" or any of the members (Joakim von Wright, Jim Grundy, or
John Harrison) at the following address:
Abo Akademi University, Department of Computer Science, Lemminkaisenkatu 14A,
20520 Turku, FINLAND; or
see the web page http://www.abo.fi/~jharriso/TPHOLs96.html.         

