\documentclass{rtaloop}
\rtalabel{ba}


\begin{document}
\begin{problem}{H. Zhang}{}{April 1991}

\begin{abstract}
Find more restrictive strategies in Boolean-ring based methods for
resolution-like first-order theorem proving.
\end{abstract}

Since the work of Hsiang \cite{H85:ai}, several Boolean-ring based methods
have been proposed for resolution-like first-order theorem proving. In
\cite{KN85:ijcai}, superposition rules were defined using multiple overlaps
(requiring unifications of products of atoms). It is unknown whether single
overlaps (requiring only unifications of atoms) are sufficient in these
inference rules. Also, it is not known if unifications of maximal atoms (under
a given term ordering) suffice. (The same problem for Hsiang's method was
solved positively in \cite{MS88:seki}\cite{Z91:iowa}.) In other respects, too,
the set of inference rules in \cite{BD87:lics,KN85:ijcai} may be larger than
necessary and the simplification weaker than possible.

\end{problem}
\end{document}