\documentstyle[11pt]{article}
\thispagestyle{empty}
\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.\ 29 \hspace{4.1in} May 1995}\\
\rule{6.3in}{.02in}
\end{center}

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

\vspace{.1in}
In keeping with the role of AAR as the ``parent'' corporation for CADE,
this issue includes several articles related to CADE.
Of especial interest is the response of Alan Bundy, current CADE
president, to proposed major changes to the CADE organization.
Also included are a solicitation for sites for the next CADE conference and
minutes of the July 1994 CADE meeting. 

I call your attention to the forthcoming QED Workshop.
When I attended the first workshop, held at Argonne, 
I found the QED concept exciting.
I hope that this second workshop will lead to specific projects that
will make QED a reality.   

Finally, I welcome the approximately fifty new members who have joined AAR since January.
I invite each of you---as well as our long-time members---to submit articles
to the {\it AAR Newsletter.} Usually, we devote much of the newsletter to  
technical articles, including challenge problems, new theorem provers, and
answers to previously open questions.
Our intention is, of course, to stimulate discussion and to advance the field
of automated reasoning.

\vspace{.2in}
\begin{center}
{\Large \bf In Defense of the CADE Organization}\\
{\it Alan Bundy}
\end{center}


% From bundy@aisb.ed.ac.uk Fri Mar 17 05:19:09 1995
% Date: Fri, 17 Mar 95 12:18:20 GMT
% From: Alan Bundy <bundy@aisb.ed.ac.uk>
% Subject: Plaisted article: new latex source
% To: veroff@cs.unm.edu
% Phone: 44-131-650-2716
% Fax: 44-131-650-6516
%


In {\it AAR Newsletter} No.\ 28, David Plaisted called for democratic
elections of the Trustees of CADE Inc. The Trustees have asked
me, as President, to respond. I do not intend to take a position
for or against David's proposal, but merely to sketch in some of
the history of these matters and to discuss some of the details
in David's proposal. I hope other people will argue the pros and
cons of the proposal through the pages of this newsletter. We need
an informed debate to arrive at a well-considered decision.

\section{The History of the CADE Organization}

Until CADE-12, CADE conferences were arranged in an informal
manner. The Program Committee of CADE-$n$ would select the site
and officers of CADE-$n+1$. The accumulated funds of previous CADEs
would be passed from Program Chair $n$ to Program Chair $n+1$,
who would personally open a bank account for it. These informal
arrangements seemed unsatisfactory to many of us for two main
reasons. First, the current CADE officers were at considerable
financial risk. If a CADE were to realize a loss, they were
personally liable. Second, the transfer of money from CADE to
CADE was wide open to abuse. No one would want to question the
personal integrity of any of the officers of CADEs, but it was
unfair both on them and on CADE members that large sums of money
should change hands in this totally unregulated way.

The solution to these problems was for CADE to become
incorporated. Incorporation gave limited liability to
CADE officers and regulated the transfer of funds between CADEs.
This move was decided by the CADE-11 Program Committee.
A corporation, CADE Inc., was created with a president, vice
president, treasurer, and secretary and a Board of Trustees. CADE
Inc. holds the central account; it lends money to each CADE
conference; and it receives any residual money, including
profits, on the completion of each CADE. CADE activities are now
governed by a set of bylaws.

Considerable discussion preceded the new arrangements. Most
people were happy with the way previous CADEs had been organized
and did not want to give up the collegiate spirit that
underpinned it. In particular, some people argued strongly that
they did not want CADE to become ``political'' or ``bureaucratic.''
They especially did not want the negative campaigning or
self-aggrandizement that might come with elections. These
arguments strongly influenced the manner in which CADE was set
up. In particular, the Program Chairs of previous CADEs were
thought to represent an experience bank of both the administrative
details and the collegiate spirit of CADE organization. So the
Program Chairs of the past four CADEs formed the core of the
Trustees.


\section{Decision Making in CADE}

The model for the CADE bylaws came from IJCAI. This was because
many of us were familiar with the IJCAI organization, and it
seemed to work well. Another organization might have done equally
well as a model, but at that point nobody advanced one.  The
IJCAI bylaws were rather legalistic and unwieldy, so we tried to
simplify them as much as we could.

Both CADE and IJCAI faced difficult problems in deciding who its
members were. The attendees at any given conference are heavily
biased by its location and are not really representative of its
overall constituency. Moreover, it is administratively difficult
to keep track of such a constantly changing membership.  IJCAI
solved this problem by creating an Executive Committee of the
Great and the Good, consisting of presidents of national
societies, editors of major journals, etc. This Executive
Committee decides the location and officers of societies and
elects Trustees to office.  As far as the election of Trustees
goes, the IJCAI election is something of a formality. The
Executive Committee is told that it is the tradition to elect the
outgoing Conference Chair and that not to do so would be
interpreted as a vote of no confidence. The result of the
election is then a foregone conclusion. This was one of the
aspects of the IJCAI bylaws that we simplified, by giving all the
powers of the Executive Committee to the Trustees and by making
the outgoing Program Chair an ex officio Trustee. We felt that
the Trustees were a more representative body to choose the
location and officers of CADEs than the outgoing Program
Committee, whose members are chosen by one individual.  By making
the Trustees consist of previous CADE Program Chairs, we ensured
that the Board had an accumulated wisdom of CADE organization
that could be drawn on by the current CADE officers.  As for
membership of CADE, we had a simple solution available, namely, to
use the membership of AAR.  This ensured a constant and easily
tracked membership, which was pretty representative of the
regular CADE attendees. CADE Inc was thus incorporated as a
subcorporation of AAR.

The bylaws of CADE can be changed by a vote of CADE members at a
general meeting. A general meeting is called at each CADE. The
quorum of this meeting is the members present, and the bylaws can
be changed by a simple majority. Proxy votes are allowed.  The
intention to raise a motion changing the bylaws must be announced
in advance of the meeting.  So the next regular opportunity to
change the bylaws, e.g., to introduce elections for
Trustees, will be at the general meeting of CADE-13 in 1996. It
is also possible to convene a special members meeting before that
date, but then the quorum becomes 20\% of the overall membership,
which might be difficult to achieve except at CADE conferences.  From
these arrangements it can be seen that the ultimate power to
determine CADE policy does already lie within the democratic
control of the membership. It is not true, as David claims, that
``there is no democratic element at all in the current system.''

\section{Detailed Comments on Plaisted's Proposal}

David Plaisted raises a number of issues about the organization
of CADE and the method of choosing Trustees. Below I discuss some
of these issues.

\begin{description}

\item[Election Mechanism:] David proposes an election by e-mail.
This would certainly simplify the process, but it would
disenfranchise some people. Most members of CADE have e-mail
access, but not all do. If we are to have truly democratic
elections, we will have to include postal votes too. This
will complicate matters, but not impossibly. We do need to
seriously consider the costs of an election. CADE Inc. has a
pretty modest bank balance.

\item[Franchise:] David proposes an election by a combination of
AAR members and recent CADE attendees. At the moment CADE
membership is coincident with AAR membership. To allow non-AAR
CADE attendees to vote would require first changing the bylaws
defining membership then inviting attendees at selected previous
CADEs to vote. In practice, two CADE general meetings would be
required to realize this.  There is also the problem of tracking
past CADE attendees.  We have not made a practice of maintaining
records, so some research would be required to find out who these
people were.

\item[Size and Number of Committees:] David proposes having both
a Board of Trustees and an Executive Committee. He does not give
a reason for this duplication, and it seems an unnecessary
complication to me. He also proposes that the Trustees be a much
larger committee than the current nine members. There is a balance
to be struck between being large enough to be representative and
small enough to be manageable. Nine members seems to me to be about
the right size.

\item[Number of Elected Positions:] David proposes electing four
Trustees every two years, with a term of four years. Thus a total of eight
elected Trustees would be in office at any one time. To this must
be added any ex officio members, e.g., the secretary and
treasurer, the current, and the future CADE officers. This might add
another four to six members, thereby giving a committee size a little
larger than I would be happy with, but not unreasonably large.
However, a term length of four years is not long when one takes into
account the need to maintain group memory and continuity. The
current term is effectively ten years, but will automatically
gradually drop to six years when we move to annual CADEs. (The past
four Program Chairs are Trustees plus the forthcoming ones. CADE's
officers are generally chosen two years in advance.)  If we
maintained current practice except for choosing Trustees by
election, we would elect only one Trustee per conference.

\item[Power of the Trustees:] David paints a rather exaggerated
picture of the power of the CADE Trustees. Once chosen, the
Program Chair and Local Arrangements Chair are collectively
responsible for the organization of each CADE.  Even if ``a
subarea or subphilosophy of CADE from [became] disproportionately
represented'' among the Trustees, this would be unlikely to
affect the distribution of papers, since accept/reject decisions
are decided by the Program Committee and the referees. If the
center of gravity of CADE was forced to move against the wishes
of its members, the conference would surely die. The
Trustees are unlikely to commit such collective suicide.

\end{description}

\section{Conclusion}

Democratic mechanisms are already in place for the members of
CADE to change the method of choosing the CADE Inc. Trustees.
Anyone who feels strongly about this can propose an appropriate
amendment to the bylaws at the next general meeting at CADE-13 in
1996. I invite anyone who intends to propose such an amendment to
publish it in the {\it AAR Newsletter} well in advance of CADE-13. We
all need to see and argue about the details of any change to
ensure that we get them right.

The present arrangements were a compromise between those who
wanted to maintain the original collegiate organization of CADE
and those who wanted to introduce some regulation and
accountability. The introduction of elections will move CADE
further away from the collegiate organization. I would not
expect such a move to be unopposed. It is vital to hear from
those who opposed change in 1992 and from anyone else who opposes
the introduction of elections. We need a full range of views to
be expressed before further change is made. Since CADE membership
coincides with AAR membership, the {\it AAR Newsletter} seems to be the
ideal forum for this debate.


\vspace{.15in}
\begin{center}
{\large \bf Proposals for Sites for CADE-14 Solicited}\\
{\it Alan Bundy, President, CADE Inc.}
\end{center} 

CADE Inc. invites proposals to host the 14th Conference on
Automated Deduction (CADE-14). CADE-14 will be held in late June
or early July 1997 outside North America.  Proposals are due by
July 1, 1995, and a final decision will be made by September 1,
1995.  Proposals will be evaluated in relation to a number of
site selection criteria, which include suitability of site and
facilities, strength of local automated reasoning research, costs,
and availability of local sponsorship. Further details are
available on request from the CADE Inc. Secretary, Neil Murray
(nvm@cs.albany.edu).



\vspace{.15in}
\begin{center}
{\Large \bf Minutes of General Meeting of CADE Inc. 1994} \\
{Friday, July 1, Nancy, France} \\
\end{center}

A general meeting of CADE Inc. took place at the end of the
CADE-12 conference. Alan Bundy was in the chair as President of
CADE Inc. About 50 people attended the meeting. These minutes
were prepared by Alan Bundy from notes taken at the time by
Claude Kirchner. Bits in square brackets are afternotes which
bring the information up to date.

\subsection*{CADE-13}

Alan Bundy announced that Michael McRobbie and John Slaney had
been chosen by the CADE Inc. Trustees as joint programme chairs of
CADE-13. CADE-13 was likely to be held as part of FLoC96, the
Federated Logic Conference, to be held at Rutgers University in
conjunction with LICS, RTA, and CAV. [This is now confirmed. The
whole conference will last from Saturday, July 27, to Saturday, August 3,
1996. CADE-13 workshops and tutorials will be on Tuesday, July 30, and
the main conference from July 31 to August 3.]

There was a suggestion from the floor to spread the conference
over 5--6 days. [Within the context of FLoC96, this was not
possible for CADE-13.] J. P. Jouannaud suggested that workshops
run concurrently with the conference. [The CADE-13 Program
Chairs have decided not to adopt this suggestion.] Attendees were
asked for proposals for new workshop topics.

\subsection*{CADE Frequency}

Alan Bundy announced that following the growth in attendance and
submissions to CADEs, the Trustees had decided to hold CADEs
annually from 1996. So CADE-14 will be held in 1997. [A call for
sites for CADE-14 has just been issued; see the preceding article.]

There followed a discussion about the problems of overlap with
RTA, which will be held annually from 1995. J. P. Jouannaud
suggested holding the two conferences in parallel. D. Dougherty
suggested coordinating them to have a six-month gap between them.


\subsection*{Evaluation of Systems and Papers}

Bob Boyer expressed concern about the evaluation of systems
described at conferences like CADE. He suggested that it be a
condition of acceptance that systems be made available via ftp.
Similar concerns were raised from the floor about other aspects
of evaluation, e.g., proofs that were too long for
inclusion in the conference paper. It was suggested that full
versions of papers be available via ftp or WWW.

Alan Bundy accepted the principle behind the point, but pointed
out that no uniform solution would fit all cases. He announced
that the Trustees had agreed that words would be inserted in all
future calls for papers to address these points. This solution
was generally welcomed.  [The Trustees have now agreed to insert
the following in all future calls:
\begin{quote}
        The Programme Committee may ask authors to furnish
        evidence of scientific claims, {\em e.g.}  computer programs,
        detailed proofs, or full experimental data.]
\end{quote}



\vspace{.15in}


\begin{center}
{\large \bf QED  Workshop II}\\
{\it Robert Boyer} (boyer@cli.com) and
{\it Andrzej Trybulec} (trybulec@cksr.ac.bialystok.pl)
\end{center}

The QED Workshop II will be held in Warsaw, Poland, on July 20--22, 1995.
The goal of this workshop is to determine whether it is possible
to change the QED Project from a fascinating concept into a practical
cooperation. 

QED is the title of an international project to build a
computer system that effectively represents much of important
mathematical knowledge and technique.  The QED system will conform to
the highest standards of mathematical rigor, including the use of
strict formality in the internal representation of knowledge and the
use of mechanical methods to check proofs of the correctness of all
entries in the system.  A principal application of the QED system will
be the verification of computer programs.  For background on the idea
of the QED Project, see ``The QED Manifesto'' in the {\it Proceedings of 
CADE 12,} {\it LNAI,} 238--251, Springer-Verlag, 1994 (also available by anonymous
ftp at ftp://info.mcs.anl.gov/pub/qed/manifesto.)  The results of the QED
Workshop I are documented in URL http://www.mcs.anl.gov/qed.


The current plan is for the workshop to be small (30 persons).  We
plan to split the workshop into one-hour discussions dedicated to
specific problems, such as the following:
\begin{itemize}

\item
 how to transform the field under consideration into a branch of
   mathematics or computer science, and what its boundaries would be,

\item
 identification of the initial mathematical targets,

\item
 identification of the fields of mathematics to be formalized,

\item
 why QED is needed by mathematics,

\item
 characterization of the likely use of the QED library by
   mathematicians,

\item
 consideration of possible use of already formalized mathematical
   knowledge,

\item
 how to organize the accumulation and reusability of mathematical
   knowledge within QED or in specified systems,

\item
 how to organize the exchange of information between systems,

\item
 how to cope with indefiniteness,

\item
 analysis of the possible use of the QED library in mathematical
   education,

\item
 database and Internet formats for retrieval,

\item
 attempt at initiating effective cooperation among projects for QED,
and

\item
 financing (potential sources) and coordination.

\end{itemize}
Each such discussion will be preceded by an introductory lecture of twenty
to thirty minutes.  We will not arrange for a presentation of individual
systems, but it is obvious that when presenting general problems we
will draw experience and examples from the systems that we know best.
We seek speakers for introductory lectures; please feel free to
propose any topic you believe is of general interest.  We are open to
any suggestions.  We will organize also a three-hour panel discussion
at the end of workshop.

If you are interested,
contact Roman Matuszewski, Workshop Chairman
(romat@plearn.edu.pl).

The QED Workshop II is hosted by
Warsaw University -- Bialystok Branch (Mizar Group),
under the auspices of the State Committee for Scientific
Research (Poland).
The co-sponsor is the Office of Naval Research (USA).


\vspace{.15in}


\begin{center}
{\Large \bf Information on Isabelle}
\end{center}

\vspace{.15in}
\noindent
{ \bf Introduction to Theorem Proving, Using Isabelle}

On July 12--14, 1995,
a course on Isabelle will be offered
at Cambridge, England, immediately prior to Mathematics
of Program Construction (MPC '95) Conference.
The course uses lectures and practical sessions to teach
students how to use the Isabelle system to perform proofs in higher-order
logic. 
Topics include single-step proof checking, forward and backward
proof, declaring types and constants, quantifier reasoning, higher-order
logic in Isabelle, and advanced proof tools.
The lecturer is  Lawrence C Paulson, originator of Isabelle.
The cost of the three-day course
is 650 pounds sterling (350 pounds for academics) plus accommodation.
Technical correspondence should be addressed to  Lawrence C Paulson, Computer Laboratory,
Pembroke Street, Cambridge CB2 3QG, England; e-mail lcp@cl.cam.ac.uk.
Administrative correspondence should be addressed to
The Registration Administrator,
Program for Industry, 1 Trumpington St, Cambridge CB2 1QA, England.
tel. +44 (0)1223 302233s; e-mail: rjs1008@cus.cam.ac.uk.
For details about the course, see the World Wide Web,
URL http://www.cl.cam.ac.uk/users/lcp/isabelle-course.html.



\vspace{.15in}
\noindent
{\bf Isabelle Users Workshop}

An Isabelle Users Workshop will be held on September 18--19, 1995, in Cambridge, UK.
The purpose of the workshop
is to allow Isabelle users to exchange techniques and results.
Both finished work and work in progress can be reported.  There will be a
program of short talks and possibly demonstrations.  A printed proceedings
will be produced provided enough papers are submitted.  There will be no
formal refereeing; within reason, all talks and papers will be accepted.
There will also be time for informal discussions.

We expect to arrange college accommodation for participants at a cost
of less than 50 pounds (UK) per day, inclusive of all meals.  As an alternative, we
can supply a list of hotels.  There will be a small registration fee.

The workshop immediately precedes HOA '95 and LOPSTR '95.
Those interested in attending
should contact
Lawrence C. Paulson, University Lecturer,
Computer Laboratory, University of Cambridge,
Pembroke Street, Cambridge CB2 3QG, England;
tel: +44(0)21223 334623,   fax: +44(0)1223 334678.
Those interested in giving a talk or demo should
send a title and
abstract.
We intend to compile the proceedings electronically from papers submitted in Postscript format.
The deadline for abstracts is June 1, 1995, and the deadline for proceedings
papers is July 1.  






       



\vspace{.15in}
\begin{center}
{\Large \bf Announcements}
\end{center}


\vspace{.15in}
\noindent
{\bf Seventh European Summer School in Logic Language and Information}


The seventh European Summer School in Logic Language and Information will be
held on
August 14--25, 1995, in Barcelona.
The main focus of the Summer School is the interface between
logic, linguistics, and computation, where it concerns the modeling of
  human linguistic and cognitive abilities.  The 1995 program will
  include courses, workshops, and symposia covering a variety of topics
  within six areas of interest: logic, language, computation, logic and
  computation, computation and language, and language and logic.
For further information, contact  ESSLLI95, GILCUB, Avda. Vallvidrera 25, 08017
  Barcelona; fax +43 3 2054656; tel. +43 3 2033597; e-mail
  esslli95@gilcub.es.


\vspace{.15in}
\noindent
{\bf EMCSR 1996}

The Austrian Society for Cybernetic Studies has issued a call for papers for the
Thirteenth European Meeting on Cybernetics and Systems Research (EMCSR 96), to be held at the University of Vienna, Austria, on April 9--12, 1996.
Sessions are planned in such areas as theory and applications of artificial intelligence,
fuzzy systems, knowledge-based systems, and knowledge discovery in databases.
For further information, contact the program chairman Robert Trappl, Department of
Med. Cybernetics and Artificial Intelligence, University of Vienna, Freyung 6/2,
A-1010 Vienna, Austria; e-mail sec@ai.univie.ac.at.
More details are also available on the World Wide Web at http://www.ai.univie.ac.at/emcsr/. 


\vspace{.15in}
\noindent
{\bf FLoC'96}

The 1996 Federated Logic Conference will be held on 
Saturday, July 27, through Saturday, August 3, 1996,
at Rutgers University, New Brunswick, New Jersey, USA.
The goal of FLoC is to battle
  fragmentation of the technical community by bringing together
  synergetic conferences that apply logic to computer science.  The
  following conferences will participate in FLoC: CADE (Conference on
  Automated Deduction), CAV (Conference on Computer-Aided
  Verification), LICS (IEEE Symposium on Logic in Computer Science),
  and RTA (Conference on Rewriting Techniques and Applications).
DIMACS will host the meeting as part of its Special Year on
  Logic and Algorithms.
For further information see the World Wide Web URL
  http://www.research.att.com/lics/FLoC.
\end{document}
