\documentclass{rtaloop}
\rtalabel{contextual-deduction}


\begin{document}
\begin{problem}{U. Reddy, F. Bronsard}{}{}


\begin{abstract}
  Is there a notion of ``complete theory'' for which \emph{contextual deduction} is
  complete for refutation of ground clauses?
\end{abstract}
  
  In \cite{BR90:lncs} a rewriting-like mechanism for clausal reasoning
  called ``contextual deduction'' was proposed.  It specializes
  ``ordered resolution'' by using pattern matching in place of
  unification, only instantiating clauses to match existing clauses.
  Does contextual deduction always terminate?  (In \cite{BR90:lncs} it
  was taken to be obvious, but that is not clear; see also
  \cite{NO90:concordia}.)  It was shown in \cite{BR90:lncs} that the
  mechanism is complete for refuting ground clauses using a theory
  that contains all its ``strong-ordered'' resolvents.  Is there a
  notion of ``complete theory'' (like containing all strong-ordered
  resolvents not provable by contextual refutation) for which
  contextual deduction is complete for refutation of ground clauses?
  
  Contextual deduction as defined in \cite{BR90:lncs} does not
  terminate.  Bronsard and Reddy have gone on to solve this
  \cite{Bronsard-Reddy-reduction} by using a more restricted,
  decidable mechanism.  A completeness proof, incorporating equational
  inference with complete systems, is given in \cite{Bronsard-thesis}.

\end{problem}
\end{document}