\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. 24 \hspace{4.1in} November 1993}\\
\rule{6.3in}{.02in}
\end{center}

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

After seven years, 
Bill McCune has
resigned as AAR Secretary.
This issue of the 
{\it AAR Newsletter}
includes an introductory note from 
the association's new secretary, Bob Veroff.
I encourage you to read his note and 
besiege him with mail---with dues, with requests for receiving the newsletter
via ftp, and so on. 

I am also delighted to include the
announcement that
Hantao Zhang has received an NSF National Young Investigator's award.
As this award indicates,
the field of
automated reasoning is clearly gaining national attention.
The AAR welcomes further announcements of this type, as well
as articles designed to stimulate further research
or to report on recent successes. 

One such article, included at the end
of this newsletter, features a set of challenge problems.
Good luck in solving them!


\vspace{.2in}
\begin{center}
{\bf New Secretary for AAR}\\
{\it Bob Veroff}\\
Dept. of Computer Science, University of New Mexico, Albuquerque, NM  87131\\
phone: (505) 277-4231; fax: (505) 277-6927; e-mail: veroff@cs.unm.edu
\end{center}

I have recently taken over from Bill McCune as secretary of AAR. 
I thank 
Bill for his efforts as secretary and for helping me become familiar with the
responsibilities of the position.  My main tasks as secretary will be to
maintain the membership list, to beg and/or harass people to stay current with
their dues, and to work with Gail Pieper to put out the AAR newsletter.

As of September 30, 1993, we have 328 members.  Unfortunately, far too many members
are behind in their dues. 
I underscore the message from the AAR president that
you bring your membership up to date; the
association bank account is dwindling.  Dues are \$7.00 for one year, \$13.00
for 2 years, and \$18.00 for three years.  Send dues to me, payable in US
dollars to the ``Association for Automated Reasoning".

Remember that you now have the option of receiving the AAR newsletter by
e-mail instead of on paper.  We also will make AAR newsletters available
by anonymous FTP.  Very few people have taken us up on this offer.  Send
me mail if you wish the details.

We may occasionally wish to contact AAR members
about articles or new procedures.
We
have e-mail addresses for only about 100 of the 328 members.  Please send me
your e-mail address if you think we may not have it and if you don't mind
having it included in our membership database.


\vspace{.3in}
\begin{center}
{\bf Congratulations to Hantao Zhang}\\
{\it Deepak Kapur}\\
State University of New York at Albany\\
Albany, NY  12222\\
kapur@cs.albany.edu
\end{center}

I am very happy and proud to inform you that Professor Hantao
Zhang, University of Iowa, is the recipient of the NSF National
Young Investigator (previously known as President's Young
Investigator) award this year.  As far as I know, Hantao is the
first one selected for this award in the field of automated
reasoning, which makes this a double honor for Hantao. And, this
also reflects well for the field of automated reasoning.

As some of you may know, Hantao and I have been working together
on the theorem prover RRL (Rewrite Rule Laboratory) since 1985.
I was lucky to have Hantao as my student and now as a
collaborator.

I wish him more such honors and awards in his illustrious career.

\vspace{.2in}
\begin{center}
{\normalsize\bf On the Least Herbrand Model for Conditional Horn Sets}\\ 
\bigskip
{\it Tie-Cheng Wang}\\
Kestrel Institute, 3260 Hillview Avenue, Palo Alto, CA 94304\\
wang@kestrel.edu
\end{center}

\medskip
\noindent The least Herbrand model plays a central role in the theory 
of logic programming and constrained resolution. It is a 
well-established result [1, 2] that for every Horn set S,
the intersection $M_{S}$ of all Herbrand models of $S$ 
is a model of S, called the least Herbrand model of S, 
and the members of $M_{S}$ are precisely those that 
are logical consequences of $S.$ In this note, we
present an extension of this result to conditional Horn sets (cHs).

We shall divide the entire set of atoms of the first-order language
under this discussion into two disjoint subsets, namely, $R$-atoms
and $K$-atoms. Let $R$-Hb be the set of ground atoms of $R$-atoms 
and let $K$-Hb be the set of ground atoms of $K$-atoms.
Then $R$-Hb $\cup$ $K$-Hb is the Herbrand base of 
the language, and each Herbrand interpretation is a 
subset of $R$-Hb $\cup$ $K$-Hb.
A set $S$ is called a {\it conditional Horn set} (cHs) wrt
$R$-atoms iff the restriction of $S$
on $R$-atoms, $S|_{R-atoms},$ is a Horn set.
According to this definition, we shall write each clause of a cHs 
in a form of $D/H/R,$ where $D$ is a member of $R$-atoms,
$H$ is a conjunction
of literals, whose atoms are members of $K$-atoms,
and R is a conjunction of members of $R$-atoms.
An ordinary Horn set $S$ can be viewed as a special
cHs, for which $S|_{R-atoms}$ is identical to $S.$
The concept cHs is a nontrivial extension of 
Horn set because a cHs as the whole may not be
a Horn set and may not be able to be transformed into a Horn set.
For a real application, a (non-Horn) cHs may be needed
for accurately specifying the typing structure of a program,
which contains predicate subtypes (i.e.,
$x:nat/0 \leq x/ x:int$) or partial functions (i.e.,  
$div(x,y):int/y \neq 0/x:int\wedge y:int$).

The problem under study here is as follows: given
a cHs S, determine whether $S$ has a least Herbrand model in a sense similar
to that for Horn set. Stated more precisely,
\begin{quote}
Let $S$ be a cHs, $B$ a subset of $K$-Hb, and
$M$ a subset of $R$-Hb. $M$ is called 
a $B$-based {\it conditional Herbrand model}
(cHm) of $S$ iff $B \cup M$ is a Herbrand model of $S.$ 
$M$ is called a least $B$-based cHm of $S$ iff
$M$ is a $B$-based cHm of $S,$ which equals the intersection
of all $B$-based cHms of $S.$ Our question is: for every
$B \subset K$-Hb, if such a least B-based cHm exists,
how can it be constructed, what properties does it possess, 
and what usage may it have? 
\end{quote}

Recall that for a Horn set $S$ (on $R$-atoms), 
the least Herbrand model of $S$ 
can be constructed as a set $\{d \in R$-$Hb \ | \ S \models d \}.$
By a straightforward extension of this result, one may 
conjecture that $M \equiv \{d \in R$-$Hb \ | \ B \cup S \models d \}$ is
the least B-based cHm. However, this conjecture is incorrect. 
Consider the cHs $S_{0} \equiv \{d_{0}/ \neg p_{0}\}$ wrt $R$-atoms.
(Assume for $i \equiv 0,1,...,$ $d_{i} \in R$-Hb, $p_{i} \in
K$-Hb.) Let $B_{0}$ be the empty set $\phi.$
Since none of atoms of $R$-Hb is a consequence 
of $B_{0} \cup S_{0}$, $M$ will be $\phi$ by the conjecture.
But $\phi$ is not a $B_{0}$-based cHm of $S_{0},$ because
$B_{0} \cup \phi \equiv \phi,$ and $\phi$ is not a model of $S_{0}.$ 

\bigskip 
{\bf Definition 1.} Let $S$ be a cHs wrt $R$-atoms, 
and let $r_{0}$ be a conjunction on $R$-Hb.
Let $(S)_{gr}$ be the entire set of ground instances of clauses of $S.$ 
Define the set of {\it ground Horn preconditions} of $r_{0}$ in $S$ by
\[
gHp(S, r_{0}) \equiv \left\{ 
       {\begin{array}{ll}
           h_{1} \wedge ... \wedge h_{n}  \ 
        \left| \ 
            {\begin{array}[m]{l}
             \{d_{1}/h_{1}/r_{1}, ...,  d_{n}/h_{n}/r_{n}\} \subset
(S)_{gr} \ {\rm and\/} \\
	     \{d_{1}//r_{1}, ..., d_{n}//r_{n}, \neg r_{0}\} \ 
{\rm is \ mini{\rm -\/}unsatisfiable\/}
          \end{array}}
        \right.
     \end{array}}
 \right\},
\]

\noindent and define the 
{\it weakest Horn precondition} (wHp) of $r_{0}$ in $S$ by
$$wHp(S, r_{0}) \equiv \bigvee_{W \in gHp(S, r_{0})}(W). \rule{3.5in}{0in}$$

Intuitively, a member of $gHp(S, r_{0})$ is a condition
under which $r_{0}$ is implied by $S,$ and $wHp(S, r_{0})$ 
is the weakest condition under which $r_{0}$ is implied by $S.$
(We use $true$ for empty clause, $false$ for empty literal, 
$D/true/R$ for $D//R$, and $D/H$ for $D/H/true.$)

{\bf Example 1.} For $S_{0} \equiv \{d_{0}/ \neg p_{0}\},$ $gHp(S_{0}, d_{0}) \equiv \{\neg p_{0}\}$ , and
$wHp(S_{0}, d_{0}) \equiv \neg p_{0}.$ 

\smallskip
{\bf Example 2.} Let
 $S_{1} \equiv \{d_{1}, d_{2}/p_{1}, d_{3} /p_{1} \wedge p_{2}/d_{1},
d_{4}/\neg p_{1} \wedge \neg p_{2}, d_{4}/p_{3}/d_{1}, d_{6}//d_{5}\}.$

\smallskip
\begin{tabular}{ll}
$gHp(S_{1}, d_{1}) \equiv \{true\}$, & $wHp(S_{1}, d_{1}) \equiv true,$ \\
$gHp(S_{1}, d_{2}) \equiv \{p_{1}\},$ &  $wHp(S_{1}, d_{2}) \equiv
p_{1},$ \\
$gHp(S_{1}, d_{3}) \equiv \{p_{1} \wedge p_{2}\},$ & $wHp(S_{1}, d_{3}) \equiv p_{1} \wedge p_{2},$\\
$gHp(S_{1}, d_{4}) \equiv \{\neg p_{1} \wedge \neg p_{2}, p_{3}\},$ 
& $wHp(S_{1}, d_{4}) \equiv (\neg p_{1} \wedge \neg p_{2}) \vee p_{3},$ \\
$gHp(S_{1}, d_{6}) \equiv \phi,$ & $wHp(S_{1}, d_{6}) \equiv false.$\\
\end{tabular}
\bigskip

{\bf Lemma 1.} Let $S$ be a cHs wrt $R$-atoms, $d_{j}$ an element of 
$R$-Hb, and $B$ a subset of $K$-Hb. 
If $B$ is a Herbrand model of $wHp(S, d_{j})$ 
(written by $[wHp(S, d_{j})]^{B} \equiv true$), 
then for every $B$-based cHm $M$ of $S,$ $d_{j} \in M.$

\noindent
{\it Proof.} From Definition 1 and the fact 
$[wHp(S, d_{j})]^{B} \equiv true,$ there exists
at least one element $g_{j}$ of $gHp(S, d_{j}),$
such that $[g_{j}]^{B} \equiv true.$ Then,
there exists a set, $S_{j} \equiv \{d_{j_{1}}/h_{j_{1}}/r_{j_{1}}, ...,
d_{j_{k}}/h_{j_{k}}/r_{j_{k}}\} \subset (S)_{gr},$ such that
$g_{j} \equiv h_{j_{1}} \wedge ... \wedge h_{j_{k}},$ 
and $S_{j}|_{R{\rm -atoms}} \cup \{\neg d_{j}\}$ is unsatisfiable. 
Let $d_{j_{i}}/h_{j_{i}}/r_{j_{i}}$ be
an arbitrary element of $S_{j}.$ 
Since $M$ is a $B$-based cHm of $S,$ 
$[d_{j_{i}}/h_{j_{i}}/r_{j_{i}}]^{B \cup M} \equiv true.$ 
Then since $[h_{j_{i}}]^{B} \equiv true,$
$[d_{j_{i}}//r_{j_{i}}]^{B \cup M} \equiv true.$ 
Furthermore, since $B$ shares no atoms with $d_{j_{i}}$ 
and $r_{j_{i}}$, $[d_{j_{i}}//r_{j_{i}}]^{M} \equiv true.$
Thus we conclude that $M$ is a model of $S_{j}|_{R{\rm -atoms\/}}.$ 
However, $S_{j}|_{R{\rm -atoms\/}} \cup \{\neg d_{j}\}$ is 
unsatisfiable. Then $\neg d_{j}$ must be false in $M,$
and consequently, $d_{j} \in M.$ \hfill Q.E.D.

The least $B$-based cHm for a conditional Horn set is defined in the following theorem.

{\bf Theorem 1} ({\it Least Herbrand Model Theorem for
conditional Horn sets}).
Let $S$ be a cHs wrt $R$-atoms, and 
let $B$ be a subset of $K$-Hb. Define
$$M^{B}_{S} \equiv \{d \in R{\rm -Hb\/} \ | \ [wHp(S, d)]^{B} \equiv
true \}.$$
Then $M^{B}_{S}$ must be a $B$-based cHm of $S,$ and
$M^{B}_{S}$ equals  the intersection 
of all $B$-based cHms of S. Accordingly, we call
$M^{B}_{S}$ the {\it least $B$-based cHm} of $S.$

\medskip
{\bf Example 3.} From Example 1 we have that
$wHp(S_{0}, d_{0})  \equiv \neg p_{0}.$ 
For $B_{0} \equiv \phi,$ noting that 
$[p_{0}]^{B_{0}} \equiv false,$ and 
so $[wHp(S_{0}, d_{0})]^{B_{0}} \equiv true,$ we conclude 
$$M^{B_{0}}_{S_{0}} \equiv \{d_{0} \}.$$
It is easy to verify that, $d_{0}/\neg p_{0}$ is true 
in $B_{0} \cup M^{B_{0}}_{S_{0}}$, and so
$M^{B_{0}}_{S_{0}}$ is indeed a $B_{0}$-based 
cHm of $S_{0}.$ Note also that, 
since $B_{0}$ is empty, each $B_{0}$-based cHm 
of $S_{0}$ must have $d_{0}$ as a member. Then
$M^{S_{0}}_{B_{0}}$ must be equal to the intersection of all
$B_{0}$-based cHms of $S_{0}.$

\bigskip

{\bf Example 4.} For the set $S_{1}$ given earlier, we present
the $B$-based least cHm of $S_{1}$ for different subset $B$ of
$K$-Hb in the following table. 

\[
\begin{tabular}{|l|l|l|l|l|l|} \hline
\rule{1cm}{0cm} & $B$ & $M^{B}_{S_{1}}$ & $B \cup M^{B}_{S_{1}}$ &
$[S_{1}]^{B \cup M^{B}_{S_{1}}}$  \\ \hline\hline
1. & $\{\}$ & $\{d_{1}, d_{4}\}$ & $\{d_{1}, d_{4}\}$ & true  \\ \hline
2. & $\{p_{1}\}$ & $\{d_{1}, d_{2}\}$ & $\{p_{1}, d_{1}, d_{2}\}$ & true \\ \hline
3. & $\{p_{1}, p_{2}\}$ & $\{d_{1}, d_{2}, d_{3}\}$ & $\{p_{1}, p_{2},
d_{1}, d_{2}, d_{3}\}$ & true \\ \hline 
4. & $\{p_{3}\}$ & $\{d_{1}, d_{4}\}$ & $\{p_{3}, d_{1}, d_{4}\}$ & true \\
\hline
5. & $\{p_{1}, p_{2}, p_{3}\}$ & $\{d_{1}, d_{2}, d_{3}, d_{4}\}$ & 
$\{p_{1}, p_{2}, p_{3}, d_{1}, d_{2}, d_{3}, d_{4}\}$ & true\\
\hline
\end{tabular}
\]

\bigskip
\noindent
{\it Proof.} 
We now prove Theorem 1 by the following two steps.

{\it Step 1.} We first prove that $M^{B}_{S}$ given in Theorem 1 is a
$B$-based cHm of $S.$ Assume that $M^{B}_{S}$ is not a $B$-based cHm of $S.$ 
We are going to deduce a contradiction from
this assumption. Let $I \equiv B \cup M^{B}_{S},$ then 
there exists at least one member $d_{0}/h/d_{1} \wedge ... \wedge d_{n}$
of $(S)_{gr}$ which is false in $I.$ Hence
we must have $[d_{0}]^{I} \equiv false,$ $[h]^{I} \equiv true,$ and  
for every $j, 1 \leq j \leq n,$ $[d_{j}]^{I} \equiv true.$ 
Since $d_{j} \not\in B$,
$[d_{j}]^{I} \equiv true$ implies that $[d_{j}]^{M^{B}_{S}} \equiv true.$ 
Then from the definition for $M^{B}_{S},$ 
$[wHp(S, d_{j})]^{B} \equiv true$. 
From Definition 1, there exists at least one element 
$g_{j}$ of $gHp(S, d_{j})$ which is true in $B.$ 
Consequently, there exists a set $S_{j} \subset (S)_{gr},$
 $S_{j} \equiv \{d_{j_{1}}/h_{j_{1}}/r_{j_{1}}, ...,
d_{j_{k}}/h_{j_{k}}/r_{j_{k}}\},$ such that
$g_{j} \equiv h_{j_{1}} \wedge ... \wedge h_{j_{k}},$ 
and $S_{j}|_{R{\rm -atoms\/}} \cup \{\neg d_{j}\}$ is mini-unsatisfiable. 
Let $S_{0} \equiv S_{1} \cup ... \cup S_{n} \cup 
\{d_{0}/h/d_{1} \wedge ... \wedge d_{n}\}.$ 
$S_{0}|_{R {\rm -atoms\/}} \cup \{\neg d_{0}\}$ must be unsatisfiable. 
Let $S'_{0} \equiv \{d^{1}/h^{1}/r^{1},...,d^{s}/h^{s}/r^{s}\}$ be
a subset of $S_{0},$ such that $S'_{0}|_{R{\rm -atoms}} \cup \{\neg d_{0}\}$
is mini-unsatisfiable. Then $g' \equiv h^{1} \wedge ... \wedge h^{s}$
must be a member of $gHp(S, d_{0}),$ and hence a disjunct of $wHp(S, d_{0}).$
However, each conjunct $h^{l}$ of $g'$ must be either $h$
(if $h^{l}$ comes from $d_{0}/h/d_{1} \wedge ... \wedge d_{n}$)
or a conjunct $h_{j_{i}}$ of $g_{j}$ for some $j, 1 \leq j \leq n, 
j_{1} \le j_{i} \le j_{k}$
(if $h^{l}$ comes from an element of $S_{j}$).
For each case, it is easy to determine $[h]^{B} \equiv true,$ 
and so we conclude that $[g']^{B} \equiv true.$  
Since $g'$ is a disjunct of $wHp(S, d_{0}),$
$[wHp(S, d_{0})]^{B} \equiv true.$ Consequently,
$d_{0} \in M_{B}^{S},$ and $[d_{0}]^I \equiv true.$ 
This result contradicts the earlier assertion 
that  $[d_{0}]^I \equiv false.$

{\it Step 2.} We now prove that $M^{B}_{S}$ equals
the intersection of all $B$-based cHms of $S.$ With the 
assertion proved in Step 1, we need only to prove a conjecture
that for every $B$-based cHm $M$ of $S$, $M^{B}_{S} \subset M.$ 
But this conjecture follows directly Lemma 1. 
\hfill Q.E.D.

\medskip

Proposition 1 given below states that Theorem 1 is a 
generalization of the classical least Herbrand model 
theorem for Horn sets. 
Proposition 2 states a relation between 
the least $B$-based cHm of a cHs $S$ and 
the least Herbrand model of the Horn set $S|_{R{\rm -atoms}}.$

\smallskip
{\bf  Proposition 1.} If $S$ is a Horn set on $R$-atoms, then
for every subset $B$ of $K$-Hb, $M^{B}_{S}$ 
defined in Theorem 1 is the ordinary least Herbrand model
of $S.$

\noindent
{\it Proof.} Since $S$ is a Horn set on $R$-atoms, each member of $S$
must be of form $D/true/R.$ Then for every element $d$ of $R$-Hb,
if $S \models d,$ then $gHp(S, d)$ must be 
the set $\{true\},$ and so
$wHp(S, d) \equiv true.$  If $S \not\models d,$ 
then $gHp(S, d)$ must be the set $\phi,$ and so $wHp(S, d) \equiv false.$
Thus, the condition $[wHp(S, d)]^{B} \equiv true$ for
$d$ being a member of $M^{B}_{S}$ is equivalent to the
condition that $d$ is a logical consequence of $S.$
\hfil Q.E.D.

\smallskip
{\bf  Proposition 2.} Let $S$ be a cHm wrt $R$-atoms and 
let $M_{0}$ be the least Herbrand model of $S|_{R{\rm -atoms}}.$ 
For every $B \subset K$-Hb, $M^{B}_{S}$ must be a subset of 
$M_{0}.$

\noindent
{\it Proof.} Trivial.  \hfil Q.E.D.

The least Herbrand model theorem for conditional Horn sets
was used by the author in proving the completeness of some 
specialized proof procedures for deduction with 
constrained theories which are conditional Horn sets. 

\bigskip
\noindent{\bf References}
\begin{enumerate}
\item M.~H.~van Emden and R.~A.~Kowalski, ``The semantics of predicate
logic as a programming language,'' {\it J. ACM}  \ 23(4) (Oct. 1976),
733--742.
\item J.~W.~Lloyd, {\it Foundations of Logic Programming,}
Springer-Verlag, New York (1984).
\end{enumerate}


\vspace{.2in}
\begin{center}
{\bf New Journal Announced}
\end{center}

We have received an announcement that a new journal,
entitled the {\it Electronic Journal of Functional \& Logic Programming} (EJFLP),
will begin publication in late 1993.
The journal is fully
refereed and will be available via e-mail free of charge.
For subscriptions, send an empty message to  
subscriptions@ls5.informatik.uni-dortmund.de.

Papers are solicited in functional and logic languages; integration of 
programming paradigms; parallelism in functional and logic programming;
program interpretation, compilation, and transformation; static analysis;
semantic foundations; proof calculi for functional, logic, and constraint 
programming; applications; and declarative programming concepts and methodology.
Papers should be submitted in postscript or dvi format
to submissions@ls5.informatik.uni-dortmund.de.  E-mail an empty message
with ``Help" in the subject field for submission information.

Members of the EJFLP Editorial Board include
R. Loogen, H. Kuchen, M. Hanus, M. MT Chakravarty, 
M. Koehler, Y. Guo,  M. Rodriguez-Artalejo, A. Krall, A. Mueck, T. Ida, 
H. C. R. Lock, A. Hallmann, P. Padawitz, C. Brzoska, and F. Pfennig. 

\vspace{.2in}
\noindent
\begin{center}
{\bf New Center for Basic Research in Computer Science}
\end{center}

A new Center for Basic Research in Computer Science (BRICS)
will be established at
Aarhus University, in association with Aalborg University, Denmark.
The center is to begin in January 1994 for a duration of at least five years.
Yearly support of about 1 million US\$ will be provided by the Danish 
National Research Foundation.  

The center will encourage research in logic, algorithmics, and semantics 
and their interplay.  It will fund visiting and postdoctoral positions and 
graduate student scholarships, and will organize seminars and meetings.
For further information, write to
Glynn Winskel or Uffe Engberg (attn. BRICS), Computer
Science Department, Aarhus University, Ny Munkegade, Bldg. 540,
DK-8000 Aarhus C, Denmark. E-mail gwinskel@daimi.aau.dk or
Fax: +45 8613 5725.


\vspace{.2in}
\begin{center}
{\bf Call for Papers}
\end{center}


\noindent
{\bf Artificial Intelligence and Mathematics} 

The 3rd International Symposium on Artificial Intelligence and Mathematics
will be held in Fort Lauderdale, Florida, on January 2--5, 1994.
This is 
a biennial series featuring applications of mathematics in artificial intelligence
as well as artificial intelligence techniques
and results in mathematics.
For further information, write to
Frederick Hoffman, Department of Mathematics, Florida Atlantic University,
P.O. Box 3091, Boca Raton, FL 33431 (hoffman@acc.fau.edu).

\vspace{.2in}
\noindent
{\bf International Conference on Logic Programming}

The 1994 International
Conference on Logic Programming
will take place in Santa Margherita Ligure, Italy, June 13--18, 1994.
The deadline for submitting papers is November 15, 1993.  
Topics include all theoretical and practical aspects of logic programming.
For further information, send e-mail to
martelli@disi.unige.it  or  pvh@cs.brown.edu.

\newpage
\noindent
{\bf CADE-12}

As we announced in the last AAR Newsletter,
the Twelfth International Conference on Automated Deduction
will take place
on
June 28--July 1, 1994,
in Nancy, France.

CADE conferences cover all aspects of automated deduction, including
first- vs. higher-order logics,
classical vs. nonclassical logics,
special vs. general-purpose inference, and
interactive vs. automatic systems.
Specific topics of interest include
resolution, sequent calculus, decision procedures,
unification, rewrite rules, and mathematical induction.
Also of interest are applications of automated deduction, including
deductive databases, logic and functional programming,
commonsense reasoning, and software and hardware development.

Papers should not exceed 15 proceedings pages; system
descriptions and problem sets should not exceed 5 proceedings
pages.  Springer style files should be used if possible; send
an e-mail with contents ``HELP'' to \verb|svserv@dhdspri6.bitnet|;
or
FTP anonymously from {\tt dream.dai.ed.ac.uk} (see
instructions in \verb|pub/cade-12/README|).
The title page of the submission should include the name, address
(with email if possible) and telephone number of each author.  Papers
must be unpublished and not submitted for publication elsewhere.
Submissions that are late or too long or that require major revision
will not be considered.

Authors should send 4 copies of their submission to the
Programme Chair
Alan Bundy,
Department of Artificial Intelligence,
University of Edinburgh,
80 South Bridge,
Edinburgh EH1 1HN,
Scotland
(Tel: [+44] 31-650-2716;
Fax: [+44] 31-650-6516) 

\begin{center}
\framebox{\begin{tabular}{ll}
Submission deadline:          & December 1, 1993 \\
Notification of acceptance:   & February 14, 1994 \\
Camera-ready copy due:        & March 29, 1994 \\
\end{tabular}}
\end{center}

\noindent
{\bf Logic in Computer Science }

The Ninth Annual IEEE Symposium on
Logic in Computer Science (LICS)
The LICS symposia aim to attract high-quality original papers
covering theoretical and practical issues in computer science that
relate to logic in a broad sense, including algebraic, categorical and
topological approaches.
Topics of interest to AAR members include
automated deduction, 
knowledge representation, lambda and combinatory calculi, logical aspects of
computational complexity, logics in artificial intelligence, logic
programming, modal and temporal logics, program logic and semantics,
rewrite rules, logical aspects of symbolic computing,
and verification.

Submission requirements are as follows: 10 hard copies of a detailed abstract 
(not to exceed 10 typed pages)
and 20 additional copies of the cover page should be
received by December 13, 1993, by the program chair:
Samson Abramsky, Attn: LICS, Department of Computing, Imperial College, 180 Queen's Gate,
London SW7 2BZ, United Kingdom (e-mail sa@doc.ic.ac.uk; phone (44) 71-589-5111 ext. 5005;
Fax: (44) 71-581-8024).
The cover page of the submission should include the title, authors, a
brief synopsis, and the corresponding author's name, address, phone
number, fax number, and e-mail address, when available.  Abstracts must be
in English, clearly written, and provide sufficient detail to allow
the program committee to assess the merits of the paper.  References
and comparisons with related work should be included.  It is recommended
that each submission begin with a succinct statement of the issues,
a summary of the main results, and a brief explanation of their
significance and relevance to the conference, all phrased for the
non-specialist.  Technical development of the work, directed to the
specialist, should follow.


\vspace{.2in}
\begin{center}
{\bf Problem Set}\\
{\it Bob Veroff}\\
University of New Mexico, Albuquerque, NM  87131\\
e-mail: veroff@cs.unm.edu
\end{center}


My students have found the following set of problems to be both challenging
and enlightening while learning to use OTTER.  Several people have asked me
for this set, so I have decided to include it in an AAR newsletter.

Consider the following definition of a Boolean algebra:
A Boolean algebra is a tuple (S,+,*,',0,1), where
S is a nonempty set of elements,
+ and * are binary operations on S,
' is a unary operation on S,
and 0 and 1 are distinct elements of S
and the following axioms hold: 

\noindent
For all x, y, and z in S,
   
{\bf A1.  Commutativity:} x + y = y + x; x * y = y * x.
    
{\bf A2.  Distributivity:}
x + (y * z) = (x + y) * (x + z);
x * (y + z) = (x * y) + (x * z).

{\bf A3.  Identity:}
x + 0 = x;
x * 1 = x.

{\bf A4.  Complement:}
x + x' = 1;
x * x' = 0.

\noindent
Prove the following theorems.
    
For all x, y, and z in S,
       
{\bf TA.  Idempotence:}
x + x = x;
x * x = x.
    
{\bf TB.  Boundedness:}
x + 1 = 1;
x * 0 = 0.

{\bf TC.  Absorption:}
x + (x * y) = x;
x * (x + y) = x.

{\bf TD.  Associativity:}
x + (y + z) = (x + y) + z;
x * (y * z) = (x * y) * z.

{\bf TE.  Uniqueness of Complement:}
if x + y = 1 and x * y = 0, then y = x'.

{\bf TF.  Involution:}
(x')' = x.

{\bf TG.  Complement of 0 and 1:}
0' = 1;
1' = 0.
    
{\bf TH.  DeMorgan's Laws:}
(x + y)' = x' * y';
(x * y)' = x' + y'.
\end{document}
