\documentstyle[jair,twoside,theapa,/usr/local/lib/tex/inputs/epsf,11pt]{article}

\def\NP{\newpage}

\jairheading{8}{1998}{39--65}{6/97}{3/98}

\firstpageno{39}

\ShortHeadings{Tractability of Theory Patching}{Argamon \& Koppel}

\parskip=1ex
\parindent=0cm
\widowpenalty=10000

\long\def\COMMENT#1{{}}
\long\def\comment#1{{}}
%\long\def\comment#1{\begin{quotation}{\tt #1 }\end{quotation}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{cor}{Corollary}
\newtheorem{defn}{Definition}

\long\def\LABFIG#1#2{\begin{tabular}{c} {#1}\\ {#2}\\ \end{tabular}}

\def\topline{{\hrule \vskip1pt \hrule height 1pt\vskip 2pt}}
\def\botline{{\vskip 2pt\hrule height 1pt \vskip1pt \hrule}}

\newenvironment{example}{\begin{quotation}\noindent{\bf Example.}}{\end{quotation}}

\def\algorithm#1#2{\subsubsection*{{\bf #1}(\hbox{#2})}}
\def\call#1#2{{\bf #1}(#2)} 

\def\proof{\noindent{\bf Proof. }}
\def\proofof#1{\noindent{\bf Proof of {#1}. }}

%\def\QED{\nobreak\hbox{\ }\hfill\hbox{\vrule width1.4ex height1.6ex}\vskip1ex\noindent}
\def\QED{\nobreak\hbox{\ }\hfill$\Box$\vskip2ex}
\def\half{\frac12}
\def\tup#1{{\langle{#1}\rangle}}
\def\open{{\Omega}}
\def\gets{\leftarrow\,}
\def\E{{\cal E}}
\def\R{{\cal R}}
\def\a{{\alpha}}
\def\BS{\backslash}
\def\IE{{\it i.e.}}

\def\LABELFIG#1#2{{\begin{tabular}{c} #1\\#2\\\end{tabular}}}
\def\IF{\leftarrow}
\def\AND{\wedge}
\def\OR{\vee}
\def\If{$\leftarrow$}
\def\And{$\,\wedge\,$}
\def\Or{$\vee$}
\def\L{{\lambda}}

\def\opens{\Omega}
\def\rev{{\bf rev}}
\def\unc{{\bf unc}}
\def\root{{\rm root}}
\def\cheap#1{{\rm Cheapest}_{#1}}
\def\cost{{\rm cost}}
\def\ul#1{{\underline{#1}}}

\def\head{{\bf head}}
\def\body{{\bf body}}
\def\entails{{\,\vdash\,}}

\def\del{{\bf delete}}
\def\addclause{{\bf add\_clause}}
\def\addante{{\bf add\_antecedent}}
\def\nullrev{{\bf null\_revision}}


\begin{document}
%\special{papersize=8.5in,11in}

\bibliographystyle{/u/segel/argamon/lib/tex/theapa}

\title{Tractability of Theory Patching}

\author{\name Shlomo Argamon-Engelson \email argamon@cs.biu.ac.il \\
	\name Moshe Koppel \email koppel@cs.biu.ac.il \\
	\addr{Department of Mathematics and Computer Science}\\
	{Bar-Ilan University}\\
	{52900 Ramat Gan, Israel}
}

\maketitle

\begin{abstract}\noindent
In this paper we consider the problem of {\it theory patching}, in
which we are given a domain theory, some of whose components are
indicated to be possibly flawed, and a set of labeled training
examples for the domain concept.  The theory patching problem is to
revise only the indicated components of the theory, such that the
resulting theory correctly classifies all the training examples.
Theory patching is thus a type of theory revision in which revisions
are made to individual components of the theory.  Our concern in this
paper is to determine for which classes of logical domain theories the
theory patching problem is tractable.  We consider both propositional
and first-order domain theories, and show that the theory patching
problem is equivalent to that of determining what information
contained in a theory is {\it stable} regardless of what revisions
might be performed to the theory.  We show that determining stability
is tractable if the input theory satisfies two conditions: that
revisions to each theory component have monotonic effects on the
classification of examples, and that theory components act
independently in the classification of examples in the theory.  We
also show how the concepts introduced can be used to determine the
soundness and completeness of particular theory patching algorithms.
\end{abstract}

\section{Introduction}

\comment{
Intuitive: Patching problem
Contrast with usual revision problem
	Preference vs. Restriction bias
Main result: Usually hard
Will introduce:
	Generalized monotonicity criterion
	Benign repair -- facilitate proofs of soundness
}

In this paper we consider the problem of {\it theory patching}, in
which we are given a domain theory, some of whose components are
indicated to be possibly flawed, and a set of labeled training
examples for the domain concept.  The theory patching problem is to
revise only the indicated components of the theory, such that the
resulting theory correctly classifies all the training examples.  Our
concern in this paper is to determine for which classes of logical
domain theories the theory patching problem is tractable.

Theory patching can be thought of as a type of theory revision in
which revisions are made to individual components of the theory.  Many
such algorithms have been investigated in the literature on theory
revision, both in machine learning
\cite{PTR-jair,either94,saitta-et-al93,wogulis91} and in inductive
logic programming (ILP)
\cite{ade-et-al94,deraedt92,wrobel94,wrobel95}.  Previous work in
theory revision has primarily been concerned with the problem of
finding the optimal revision to a theory for a given set of training
examples, according to some preference bias.  For example, a theory
revision algorithm may prefer to make the fewest number of revisions
necessary to satisfy all of the training examples.  We, however, are
not concerned with finding an optimal set of revisions, but rather
with finding {\it any} satisfying set of revisions, under the
constraint that some theory components may not be revised.

Note that if all components in a theory are revisable, the theory
patching problem is trivially solvable, since the theory can simply be
discarded and replaced by some theory which satisfies all the examples
(if such a theory exists).  Hence the problem is interesting only
because of the inductive bias consisting of restricting revision to a
subset of the input theory's components.  Such a restriction is often
used as an initial restriction on the revision process
\cite{PTR-jair,saitta-et-al93,weber-tausend94}, but also can arise
during the process of revision when an algorithm performs an
unretractable revision.  Thus the tools developed in this paper for
analyzing the theory patching problem may be applied to many theory
revision algorithms extant in the literature.  

We consider both propositional and first-order domain theories, and
show that the theory patching problem is equivalent to that of
determining what information contained in a theory is {\it stable}
regardless of what revisions might be performed to the theory.  In
particular, if some example is stably misclassified (\IE, it remains
misclassified regardless of how the theory may be revised), then the
theory cannot be patched.  We will show that although determining
stability is not tractable in general, it is tractable if the input
theory satisfies two conditions, which will be discussed in detail in
the paper.  The first condition concerns the monotonicity of the
theory under possible revisions, while the second condition concerns
the independence of theory components in the classification of
examples in the theory.

In the next section, we treat the tractability of theory patching for
propositional theories, showing that the problem is intractable in
general, but that a polynomial-time algorithm exists for a large
subclass of propositional theories.  Then in
Section~\ref{sec:first-order} we discuss what additional restrictions
suffice to ensure tractability of patching for first-order
domain-theories.

\section{Propositional Theory Patching}
\label{sec:propositional}

In this section, we address the problem of patching propositional
domain theories.  We first define the problem precisely, and then show
that the problem is NP-hard in general.  Then, in
Section~\ref{sec:prop-tractable} we provide an algorithm for reducing
the patching problem to the stability problem.  In
Section~\ref{sec:stability} we show for what class of theories the
stability problem is tractable, and give an algorithm for solving
stability for such theories.  We conclude this section by showing how
the concepts introduced can be used to determine the soundness and
completeness of particular theory patching algorithms.

\subsection{Defining the problem}

\subsubsection{Theories}

In this section, we consider cycle-free propositional definite-clause
theories with a single root proposition, allowing negation as failure
in clause antecedents.  Each clause $p\IF{l_1\AND\cdots\AND{l_n}}$
consists of a {\bf head}, $p$, and {\bf body},
${l_1\AND\cdots\AND{l_n}}$.  For a given theory $\Gamma$, we stipulate
as given a set of {\bf primitive propositions}, such that no primitive
proposition may appear in the head of a clause in the theory.
Primitive propositions serve the function of `observable facts' in the
theory.

\begin{figure}
\centerline{
\begin{tabular}{lcl}
CUP	& $\leftarrow$ & UPRIGHT \And LIFTABLE \And OPEN \\
UPRIGHT	& $\leftarrow$ & HAS-BOTTOM \\ % \And FLAT-BOTTOM \\
LIFTABLE& $\leftarrow$ & GRASPABLE \And LIGHT-WEIGHT \\
OPEN	& $\leftarrow$ & HAS-CONCAVITY \And UPWARD-CONCAVITY \\
OPEN	& $\leftarrow$ & HAS-STRAW \\
{GRASPABLE} & $\leftarrow$ & HAS-HANDLE \\
GRASPABLE & $\leftarrow$ & SMALL \And {CERAMIC} \And DRY\\
\end{tabular}
}
\caption{The CUP theory (adapted from Winston~et
al.~\protect\citeyear{winston-et-al83}).\label{fig:cup-theory}} 
\end{figure}

An {\bf example} $E$ for a propositional theory $\Gamma$ with root $r$
is a truth assignment to all the primitive propositions in $\Gamma$.
We say that $\Gamma$ {\bf covers} $E$ if $\Gamma\cup{E}\entails{r}$
(under standard resolution with negation as failure), otherwise $E$ is
termed {\bf uncovered} by $\Gamma$; let $\Gamma(E)=T$ if $E$ is
covered by $\Gamma$, and $\Gamma(E)=F$ otherwise.  Training data is
given in the form of labeled examples, where a {\bf labeled example}
is a pair $\tup{E,l}$ consisting of an example $E$ and a truth
assignment $l\in\{T,F\}$.  If $l=T$, the labeled example is termed
{\bf positive}, otherwise it is termed {\bf negative}.  The goal of
theory patching is to revise a given theory so that it covers all
given positive examples and does not cover any given negative example.

\begin{example}
Consider the ``CUP theory'' given in Figure~\ref{fig:cup-theory},
which classifies objects as cups or non-cups.  The head of the first
clause, for example, is ``CUP'' and its body is the expression
``UPRIGHT\And LIFTABLE\And OPEN''.  The primitive propositions of the
theory are HAS-BOTTOM, LIGHT-WEIGHT, HAS-CONCAVITY, UPWARD-CONCAVITY,
HAS-STRAW, HAS-HANDLE, SMALL, CERAMIC, and DRY.

Now consider the labeled example $\tup{E_1,T}$, where
$E_1$=\{HAS-BOTTOM, LIGHT-WEIGHT, HAS-CONCAVITY, UPWARD-CONCAVITY,
SMALL\}.  Although the labeled example is positive, $E_1$ is not
covered by $\Gamma$ (\IE, $\Gamma(E_1)=F$), and so the theory
needs to be revised.
\end{example}

In theory patching we are interested in considering revisions to
individual components of a theory.  We thus define the {\bf
components} of a theory $\Gamma$ to be its propositions, clauses, and
the literals in the antecedent of each clause (where separate
appearances of the same literal are considered different components).
We distinguish between a proposition itself and each of its
appearances in the theory's clause antecedents since in the course of
revision we may wish either to change the definition of a proposition
or to remove a given appearance of the proposition without changing
its definition\footnote{The corresponding distinction for a clause
with a conjunction of propositions in its head would be to either
revise the body of the clause or to delete one of the propositions in
its head.  Since we only allow a single head proposition for each
clause, this issue is not relevant here.}.

\subsubsection{Revisions}

Now we restrict which components of a theory may be revised, by defining:
\begin{defn}
A {\bf patchable propositional theory} is a pair $\tup{\Gamma,\Omega}$
consisting of a propositional domain theory $\Gamma$ and a set
$\Omega$ of components of $\Gamma$.  We call $\Omega$ the {\bf open
components} of $\tup{\Gamma,\Omega}$, terming all components of
$\Gamma$ not in $\Omega$ {\bf closed}.
\end{defn}

The only components that may be revised in a patchable theory are the
open components; the closed components must remain as is.
Intuitively, the open components are those which we believe might be
flawed, while the closed components are those which we assume are
correct as is.  How this information might be obtained is beyond the
scope of this paper; we simply assume it as given.  For example, a set
of open components could be provided by the domain expert who created
the theory.  Closing some components of the theory amounts to an
inductive bias on the learning problem, removing some possible
theories (those not obtainable by revisions to open components) from
consideration as hypotheses.

We now consider revisions to a propositional domain theory.  Roughly
speaking, we allow deletion and addition of components, but we will
need to be precise in order to ensure that revisions are local to a
component.  We first define, therefore, what exactly constitutes a
revision to a {\it specific component} as opposed to a global revision
to the theory.  We will use the notion of a {\bf simple clause}, whose
body contains literals only for primitive propositions.

\begin{itemize}
\item
We regard deletion of a component to be a revision to that component.
Thus we can revise a clause or an antecedent literal by simply
deleting it from the theory.  Note that we can think of deleting an
antecedent literal as treating the literal as if it were always true.
Hence, we naturally extend the definition to propositions by defining
deletion of a non-primitive proposition $p$ to mean the addition of a
clause for $p$ that renders $p$ always true.  (To be precise, this
has the effect of deleting every antecedent literal $p$ and deleting
all clauses containing the antecedent literal $\neg{p}$.)  We denote
by $\Gamma\BS\{c\}$ the theory resulting from the deletion of
component $c$ from $\Gamma$.

\item
We may also revise a clause in $\Gamma$ by adding a new positive or
negative literal for a new proposition, $q\not\in\Gamma$, to the body of
the clause, and adding a set of new simple clauses defining $q$ to
$\Gamma$.  (The restriction to simple clauses ensures that the effects
of the revision are local to the clause under revision.)

\item
Similarly, we may revise a proposition $p$ by adding a new clause $C$
with head $p$ to $\Gamma$, such that the propositions appearing in
$C$'s body do not appear in $\Gamma$, as well as a set of new simple
clauses defining each of those new propositions.  (As above, the
restriction to simple clauses ensures that the effects of the revision
are local to the clause under revision.)
\end{itemize}

\newpage

\begin{example}
Consider a revision to the CUP theory which (i) adds the antecedent
literal ``$\neg$ABSORB'' to the body of the first GRASPABLE clause
(changing the clause to read
``GRASPABLE$\IF$HAS-HANDLE\And$\neg$ABSORB''), and (ii) adds clauses
to the theory defining the new proposition:
\begin{itemize}
\item ABSORB$\IF$CERAMIC\And HAS-BOTTOM
\item ABSORB$\IF$HAS-CONCAVITY\And HAS-BOTTOM
\end{itemize}
This revision (call it $r_1$) is considered a revision to the first
GRASPABLE clause in the theory.  On the other hand, if the revision
included, say, addition of the clause ``ABSORB$\IF$SMALL\And OPEN', it
would {\it not} constitute a revision to the GRASPABLE clause, since
the new clause is not simple (OPEN is a non-primitive proposition in
the theory).

Similarly, consider the revision $r_2$, consisting of adding the
clauses:
\begin{itemize}
\item LIFTABLE$\IF$FITS-IN-HAND
\item FITS-IN-HAND$\IF$SMALL \And $\neg$HAS-STRAW
\end{itemize}
This revision is considered a revision to the proposition LIFTABLE,
since the clause added for the new proposition is simple.  If,
however, the revision included, say, addition of the clause
``FITS-IN-HAND$\IF$SMALL \And GRASPABLE'' it would not constitute a
revision to that proposition, since the added clause is not simple
(and hence the revision affects more than one component of the
theory). 
\end{example}

Note that in the above example, after we apply revision $r_1$, the
first GRASPABLE clause cannot be used to prove any example for which
$\neg$ABSORB is false (\IE, for which HAS-BOTTOM and either CERAMIC or
HAS-CONCAVITY are true).  If for some such example there are no
proofs in the original theory which do not use the clause being
revised, then the example will not be covered by the revised theory,
even if it was covered by the original theory.  Thus we can say that
the first GRASPABLE clause is `disabled' by the revision $r_1$ for
such examples.  Note that the revision does not change the
classification of examples for which $\neg$ABSORB is true, and hence
the clause is not disabled for those examples.

Similarly, after the application of $r_2$, the proposition LIFTABLE
cannot prevent a proof of any example for which FITS-IN-HAND is true
(\IE, for which SMALL is true and HAS-STRAW is false).  If such an
example was uncovered in the original theory only because LIFTABLE was
false, then in the revised theory the example becomes covered.  That
is, we can say that the proposition LIFTABLE becomes `disabled' for
such examples, in the sense that, for those examples, the revised
theory acts just like a theory with the proposition deleted.  For
those examples for which FITS-IN-HAND is false, however, the
proposition is not disabled by the revision.

More generally, in the case of adding a literal to a clause we can
say that the clause is effectively disabled for all examples for which
the added literal is false.  Hence, in the case of a revision to a
clause, the set of examples for which the new antecedent literal is
false is called the {\bf disabling set} of the revision.  Similarly,
in the case of a revision adding a new clause for a proposition we
can say that the proposition is effectively disabled for all examples
for which the body of the new clause is satisfied.  Hence, in the case
of revision to a proposition, the set of examples for which the body
of the new clause is satisfied is called the {\bf disabling set} of
the revision.

\comment{This intuitive idea can be
restated more formally.  We first say that $\Gamma$ is {\bf
indistinguishable from} $\Gamma'$ {\bf for} $E$ if for all
propositions ${p\in\Gamma}$, $\Gamma\cup{E}\entails{p}$ if and only if
$\Gamma'\cup{E}\entails{p}$.  (The indistinguishability relation is
assymetric, since we consider only the propositions in $\Gamma$.)
Then, for any given revision $r$ to the component $c\in\Gamma$,
$r(\Gamma)$ is indistinguishable from $\Gamma\BS{c}$ for every example
$E$ in the disabling set of $r$, and $r(\Gamma)$ is indistinguishable
from $\Gamma$ for every example $E$ not in the disabling set of $r$.}

\begin{example}
The disabling set of the revision $r_1$ described above, adding the
literal $\neg$ABSORB to the GRASPABLE clause, is the set of all
examples for which $\neg$ABSORB is false, \IE, those examples for
which HAS-BOTTOM and either CERAMIC or HAS-CONCAVITY are true.
Similarly, the disabling set of the revision $r_2$ described above,
adding the clause LIFTABLE$\IF$FITS-IN-HAND for the LIFTABLE
proposition, is the set of all examples for which FITS-IN-HAND is
true, \IE, those examples for which SMALL is true and HAS-STRAW is
false.
\end{example}

Note that any two revisions to a component that disable the same set
of examples are identical in their effects, regardless of their
syntactic form.  Thus, for our purposes a revision to a component is
defined by its disabling set.  For example, any revision that disables
a component for all examples is called `deletion', while any revision
that does not disable a component for any example is called the `null
revision'.

We will consider the general problem setting in which each component
in a theory may have a different set of revisions that may be
applied to that component.  That is, some revisions may be permitted
at certain components but not at other components.  We stipulate that
the set of {\bf permitted} revisions to a patchable theory
$\tup{\Gamma,\Omega}$ is given by a {\bf revision function} $\rho$
from each component in $\Omega$ to the set of revisions that may be
applied to that component; for a theory component $c$, $\rho(c)$ is
the set of revisions that may be applied to $c$.

The most general possible set of revisions is one in which any open
proposition or clause in the theory may be disabled for any set of
examples.  Therefore, we say that a revision function $\rho$ is {\bf
unrestricted} if for each open proposition or clause component
$c\in\Omega$ and any set of examples $\E$, there exists $r\in\rho(c)$
such that $\E$ is the disabling set of $r$.

\subsubsection{Patching}

Given a patchable theory and a set of examples, we wish to find some
theory that is consistent with the examples, such that the theory is
obtainable from the input theory by sequences of permitted revisions.
More formally:
\begin{defn}
Given a patchable theory $\tup{\Gamma,\Omega}$ and revision function
$\rho$, a theory $\Gamma'$ is \\
{\bf $\rho$-obtainable} from $\Gamma$ if, for some integer $n$, there exists a 
sequence of $n$
revisions $\R=\{r_i\}$ to respective components
$\{c_i\}\subset\Omega$, where $r_i\in\rho(c_i)$, such that \\
$\Gamma'=r_n(c_n,r_{n-1}(c_{n-1},\ldots,r_1(c_1,\Gamma)))$.
\end{defn}
For convenience, if $\rho$ is unrestricted, we drop the $\rho$ and
simply say that $\Gamma'$ is {\bf obtainable} from $\Gamma$.

The patching problem, then, is to revise open components
so that all of the
given positive and none of the given negative examples are covered by the 
new theory:

\begin{defn}
The {\bf propositional theory patching problem}
PPATCH$(\Gamma,\Omega,\rho,\E)$ is:
\begin{description}
\item[Given:] a patchable propositional theory
$\tup{\Gamma,\Omega}$, revision function $\rho$, and set $\cal E$ of labeled examples for
$\Gamma$, 
\item[Find:] a theory $\Gamma'$ which is $\rho$-obtainable from $\Gamma$
such that for all $\tup{E,l}\in{\cal E}$,  $\Gamma'(E)=l$, if such a
theory exists; otherwise, return FAIL.
\end{description}
\end{defn}
If such a $\rho$-obtainable theory exists, we say that
$\tup{\Gamma,\Omega}$ is {\bf repairable} under $\rho$ for $\cal E$.

When $\rho$ is an unrestricted revision function, we drop the $\rho$
and write PPATCH($\Gamma,\Omega,\E$).  In this case, the only
restriction on possible revisions is given by the set of open
components $\Omega$.

Note that in the case of unrestricted revisions a single revision to
each open component is in principle sufficient, since a single
revision can disable a component for an arbitrary subset of examples.
Moreover, the order of revisions is irrelevant.  Unrestricted
revisions are assumed in many theory revision systems in the machine
learning literature \cite{PTR-jair,either94,forte}, although in the
ILP literature, various restrictions on the revision function are
assumed (see Wrobel~\citeyear{wrobel95} and other works referenced
there).  In this paper the hardness (Section~\ref{sec:prop-hardness})
and soundness results (Section~\ref{sec:soundness}) hold for a wide
range of restricted revision functions, while the tractability results
(Section~\ref{sec:prop-tractability}) are shown for the case of
unrestricted revision functions.

\begin{example}
Suppose we are given a set of open components $\Omega$ for the CUP
theory consisting of the first clause for GRASPABLE and the antecedent
literal CERAMIC\footnote{Note that it is the {\it antecedent literal}
CERAMIC and not the proposition that is open here.  The primitive
proposition CERAMIC is not revisable.} in the last clause for
GRASPABLE (depicted in Figure~\ref{fig:cup-theory-opens} by
underlining).  Let us also assume as given an unrestricted revision
function.  This represents the situation in which the expert who gave
us the theory is somewhat unsure of her definition of GRASPABLE, and
so indicates that its first clause may be too permissive, and also
that the antecedent literal CERAMIC in the last clause for GRASPABLE
may not be necessary.  That is, the theory as given is the best one
the expert can currently give, but she allows that some parts of the
theory may be mistaken.  For example, the fact that the antecedent
literal HAS-HANDLE is not marked as possibly flawed means that if the
first GRASPABLE clause is included, that antecedent literal must
appear; the clause might be deleted entirely, or other antecedent
literals may be added to it, but the HAS-HANDLE antecedent literal may
not be deleted.

Consider now the example set $\cal E$ consisting of the examples:
\begin{description}
\item[$E_1$:] \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-CONCAVITY, \\
UPWARD-CONCAVITY, SMALL, DRY\}, labeled as positive,
\item[$E_2$:] \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-STRAW, HAS-HANDLE,
HAS-CONCAVITY, UPWARD-CONCAVITY, SMALL, CERAMIC\}, labeled as
negative, and 
\item[$E_3$:] \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-STRAW,
HAS-HANDLE, HAS-CONCAVITY, SMALL\}, labeled as positive, and
\item[$E_4$:] \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-STRAW, HAS-HANDLE,
HAS-CONCAVITY, UPWARD-CONCAVITY, SMALL\}, labeled as
positive.
\end{description}
The theory $\Gamma$ does not cover the example $E_1$.  However,
$\Gamma$ may be revised to cover $E_1$ by the deletion of the open
antecedent literal CERAMIC, without harming the desired
classifications of other examples in $\E$.  Similarly, although
$\Gamma$ incorrectly covers the negative example $E_2$, it can be
revised to not cover the example by the deletion of the first
GRASPABLE clause; however, such a revision would cause examples $E_3$
and $E_4$ to be incorrectly classified.  A proper revision to the
clause, that uncovers $E_2$ while keeping $E_3$ and $E_4$ covered,
would be to add the antecedent literal $\neg$X to it, along with
adding the clause ``X$\IF$SMALL\And HAS-STRAW''.  The new literal is
true for both $E_3$ and $E_4$, and so only $E_2$ is made uncovered by
the revision.  In other words, $E_2$ is in the disabling set of the
revision, while neither $E_3$ nor $E_4$ is.  Note that $E_1$ is also
disabled at the first GRASPABLE clause by this second revision, but
its classification is unchanged, since $E_1$ has a satisfactory proof
through the second GRASPABLE clause (after the first revision is
applied).

\begin{figure}
\centerline{
\begin{tabular}{lcl}
CUP	& $\leftarrow$ & UPRIGHT \And LIFTABLE \And OPEN \\
UPRIGHT	& $\leftarrow$ & HAS-BOTTOM \\ % \And FLAT-BOTTOM \\
LIFTABLE& $\leftarrow$ & GRASPABLE \And LIGHT-WEIGHT \\
OPEN	& $\leftarrow$ & HAS-CONCAVITY \And UPWARD-CONCAVITY \\
OPEN	& $\leftarrow$ & HAS-STRAW \\
\ul{GRASPABLE} & $\leftarrow$ & HAS-HANDLE \\
GRASPABLE & $\leftarrow$ & SMALL \And \ul{CERAMIC} \And DRY\\
\end{tabular}
}
\caption{The patchable CUP theory with open components
underlined.\label{fig:cup-theory-opens}}  
\end{figure}

Now consider the example:
\begin{description}
\item[$E_5$:] \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-CONCAVITY, \\
UPWARD-CONCAVITY\}, labeled as positive.
\end{description}
This example is particularly interesting because {\it no} possible
revision to $\Gamma$ can change its classification as uncovered.  That
is, the fact that $E_5$ is not a CUP (according to $\Gamma$) is
`stable', in the sense that no changes to the open components of
$\Gamma$ can invalidate the conclusion.  Thus $\Gamma$ is not be
repairable for $E_5$.  The fact that patchable theories contain such
stable information is fundamental and, as we will see below, plays a
key role in theory patching.
\end{example}


\subsection{Hardness}
\label{sec:prop-hardness}

Despite the deceptive simplicity of the problem, theory patching is
intractable for propositional theories for a wide range of revision
functions.  We say that a revision function $\rho$ for
$\tup{\Gamma,\Omega}$ {\bf allows deletion} if for all $c\in\Omega$,
$\rho(c)$ contains a revision that deletes $c$.
Clearly, if $\rho$ is unrestricted it
allows deletion.

\begin{theorem}[Propositional hardness]
For any fixed revision function $\rho$ which allows deletion,
PPATCH$(\Gamma,\Omega,\rho,\E)$ is NP-complete.
\label{thm:prop-hardness}
\end{theorem}
\proof
First, it is easy to see that PPATCH$\in$NP, since we can check in
polynomial time if a given set of revisions yields a theory satisfying
a set of labeled examples $\E$.  We show that PPATCH is NP-hard by
reducing the satisfiability problem (SAT) to propositional theory
patching.  Suppose we wish to find an assignment that makes an arbitrary CNF
formula $S$ satisfiable, where
\[
S = \bigwedge_{i=1}^{n}
	(\bigvee_{j=1}^{k_i} a_{ij}) \vee (\bigvee_{j=1}^{\l_i} \neg b_{ij})
\]
where for all $i,j,k,$ and $\l$, $a_{ij}$ and $b_{k\l}$ are (not necessarily distinct) 
propositions. 

Now let $\Gamma$ be the theory:
\[
\begin{array}{rcl}
\multicolumn{3}{c}{
\begin{array}{rcl}
   R	& \leftarrow & D_1 \wedge D_2 \wedge \cdots \wedge D_n \\
\end{array}
} \\
	&&\\
\begin{array}{rcl}
   D_1	& \leftarrow & a_{11} \\
	&  \vdots    & \\
   D_1	& \leftarrow & a_{1k_1} \\
   D_2	& \leftarrow & a_{21} \\
	&  \vdots    & \\
   D_n	& \leftarrow & a_{nk_n} \\
	&& \\
   a_{11} & \leftarrow & \ul{A_{11}} \\
	& \vdots & \\
   a_{nk_n} & \leftarrow & \ul{A_{nk_n}} \\
\end{array} &\hskip1cm&
\begin{array}{rcl}
   D_1	& \leftarrow & \neg b_{11} \\
	&  \vdots    & \\
   D_1	& \leftarrow & \neg b_{1\l_1} \\
   D_2	& \leftarrow & \neg b_{21} \\
	&  \vdots    & \\
   D_n	& \leftarrow & \neg b_{n\l_n} \\
	&& \\
   b_{11} & \leftarrow & \ul{B_{11}} \\
	&  \vdots    & \\
   b_{n\l_n} & \leftarrow & \ul{B_{n\l_n}} \\
\end{array}\\
\end{array}
\]
Note that the total number of theory components (propositions, clauses
and literals) is O($N$), where $N$ is the number of literals in
$S$. Let $\Omega$ be the set of components of $\Gamma$ consisting of
the antecedent literals in the clauses $a_{ij}\leftarrow{A_{ij}}$ and
$b_{ij}\leftarrow{B_{ij}}$.  Let $\rho$ be a revision function
permitting deletion of the antecedent literals in $\Omega$.  Let $E$ be an
example for $\Gamma$ which assigns all primitive propositions the
value $F$.

Consider now the theory patching problem
PPATCH$(\Gamma,\Omega,\rho,\{\tup{E,T}\})$, where $E$ is assigned a
positive label.  Any set of permissible revisions to components in
$\Omega$ amounts to a truth-value assignment to the propositions which
satisfies $S$.  For example, if the antecedent literal $A_{ij}$ is left alone,
the proposition $a_{ij}$ will have the value false, whereas deleting
the antecedent literal $A_{ij}$ from the clause $a_{ij}\leftarrow{A_{ij}}$
produces the clause $a_{ij}\leftarrow$, giving $a_{ij}$ the value
true.  Hence, if the theory can be repaired in polynomial time in
$|\Gamma|$, a satisfying truth assignment can also be found in
polynomial time in the size of $S$.  \QED

\begin{figure}
\centerline{
\begin{tabular}{lcl}\it
R & $\IF$ & D1, D2, D3 \\
D1 & $\IF$ & a \\
D1 & $\IF$ & b \\
D2 & $\IF$ & $\neg$a \\
D2 & $\IF$ & c \\
D3 & $\IF$ & $\neg$b \\
a & $\IF$ & \ul{A}\\
b & $\IF$ & \ul{B} \\
c & $\IF$ & \ul{C}\\
\\
 & {\rm (a)} & \\
\end{tabular}
\hskip2cm
\begin{tabular}{lcl}\it
R & $\IF$ & D1, D2, D3 \\
D1 & $\IF$ & a \\
D1 & $\IF$ & b \\
D2 & $\IF$ & $\neg$a \\
D2 & $\IF$ & c \\
D3 & $\IF$ & $\neg$b \\
a & $\IF$ & \\
b & $\IF$ & B \\
c & $\IF$ & \\
\\
 & {\rm (b)} & \\
\end{tabular}
}
\caption{Theories for the SAT problem for the formula
$S = (a\vee b) \wedge (\neg a\vee c) \wedge (\neg b)$. 
(a)~The input theory according to the construction for
Theorem~\ref{thm:prop-hardness}.  Open antecedent literals are
underlined.  (b)~The theory corresponding to the satisfying assignment
$a=$T, $b=$F, $c=$T.
\label{fig:CNF}
}
\end{figure}

For example, consider the CNF formula $S=(a\vee
b)\wedge(\neg{a}\vee{c})\wedge(\neg{b})$ and its corresponding theory
$\Gamma$ shown in Figure~\ref{fig:CNF}.  Each revision to a primitive
antecedent literal corresponds to deciding whether the head of the
corresponding clause will be true (if the antecedent literal is
deleted, giving a `fact' clause, eg ``$a\IF T$'') or false (if the
antecedent literal, and hence the false value given by $E$, is
retained).  Hence, a set of revisions to $\Gamma$ that satisfies the
labeled example $\tup{\{\neg{A},\neg{B},\neg{C}\},T}$ corresponds to a
variable assignment satisfying $S$.  For example, the revision giving
the theory in Figure~\ref{fig:CNF}(b) corresponds to the satisfying
assignment $a=$T, $b=$F, $c=$T.

\subsection{Reducing patching to the stability problem}
\label{sec:prop-tractability}
\label{sec:prop-tractable}

The hardness result above shows that for nearly any choice of revision
function, including the unrestricted case, the theory patching problem
is intractable.  In this section, we develop constructive proofs of
the tractability of special cases of theory patching with an
unrestricted revision function (as above, in the unrestricted case we
drop the parameter $\rho$ when no ambiguity results).  We do this by
first reducing the patching problem to that of finding `benign'
revisions to a component.  A benign revision to a component is one
which allows the revised component to become closed without affecting
the repairability of the theory.  We then reduce the problem of
finding benign revisions to that of determining the stability of
examples in the theory, where a stable example is one whose
classification is the same in all revised versions of the theory.
Finally, we show that determining stability is tractable provided the
theory satisfies a general monotonicity property with respect to
revision.

We begin by defining the notion of benign revision precisely:

\begin{defn}
Given a patchable theory $\tup{\Gamma,\Omega}$, a revision $r$ on a
component $c\in\Omega$ is {\bf benign} for a labeled example
$\tup{E,l}$ if $\tup{r(c,\Gamma),\Omega\BS\{c\}}$ is repairable for
$\tup{E,l}$.  Similarly, $r$ is {\bf benign} for a set $\E$ of labeled
examples if $\tup{r(c,\Gamma),\Omega\BS\{c\}}$ is repairable for $\E$.
\end{defn}

That is, a revision to a theory component is benign if the resulting theory 
is repairable for $\E$, even if the component 
becomes closed after the revision is performed (\IE, the revision is not 
retractable).
Note that if a theory is
repairable for an example set $\E$, then for each open component there
must exist a revision, possibly null, which is benign for $\E$.

\begin{defn}
The {\bf propositional benign revision problem}
PBENIGN$(\Gamma,\Omega,c,\E)$ is: 
\begin{description}
\item[Given:] a patchable theory $\tup{\Gamma,\Omega}$, a component
$c\in\Omega$, and a set of labeled examples $\E$,
\item[Find:] a revision $r$ on $c$ which is benign for $\E$, if such
exists; otherwise return FAIL.
\end{description}
\end{defn}

The key to successful theory patching is finding benign revisions.
This is seen via a simple reduction from PPATCH to PBENIGN, which is
linear in $|\Omega|$.

%\NP

\begin{theorem}
Given a patchable propositional theory $\tup{\Gamma,\Omega}$, and a
training set of labeled examples ${\cal E}$, PPATCH is 
reducible to PBENIGN in time linear in $|\Omega|$.
\label{thm:patch-benign}
\end{theorem}
\proof
The following algorithm solves PPATCH, given PBENIGN as a subroutine.
The idea is to perform a benign revision on each open component
(recall that the null revision is also a revision).

\algorithm{PPATCH}{$\Gamma,\Omega,\E$}
\begin{enumerate}
\item $\Gamma'\gets\Gamma$, $\Omega'\gets\Omega$, $\R\gets\emptyset$;
\item While $\Omega'\neq\emptyset$: \label{step:loop}
\begin{enumerate}
\item Choose $c\in\Omega'$;
\item $r\gets$\call{PBENIGN}{$\Gamma',\Omega',c,\E$};
\item If $r=$ FAIL, return FAIL;
\item $\Gamma'\gets{r(c,\Gamma')}$;
\item $\Omega'\gets\Omega'\BS{c}$;
\item $\R\gets \R\cup\{r\}$;
\end{enumerate}
\item Return $\R$;
\end{enumerate}

First note that the complexity of the algorithm is
O($|\Omega|\cdot{m}$), where $m$ is the complexity of solving PBENIGN,
since there is one call of PBENIGN for each component in $\Omega$.

Now we show that the algorithm solves PPATCH.  First suppose that
$\tup{\Gamma,\Omega}$ is repairable.  We contend that output $\R$ is a
set of revisions that produces a repaired theory from $\Gamma$, in
other words, at the end of the algorithm, $\Gamma'$ classifies all
examples in $\E$ correctly.  To see this, consider the patchable
theory $\tup{\Gamma',\Omega'}$ on each iteration of
Step~\ref{step:loop}.  Before the loop begins, $\tup{\Gamma',\Omega'}=
\tup{\Gamma,\Omega}$ and so is repairable by assumption.  After each
execution of the body of the loop, we update
$\tup{\Gamma',\Omega'}\gets\tup{r(c,\Gamma'),\Omega'\BS\{c\}}$ which
is also repairable, since $r$ is benign.  When the loop terminates,
$\Omega'=\emptyset$, hence $\tup{\Gamma',\emptyset}$ is repairable (by
the loop invariant).  Thus $\Gamma'$ must classify all examples in
$\E$ correctly, since no open components are available to repair.

Conversely, if $\tup{\Gamma,\Omega}$ is not repairable, there will be
no benign repairs to any components, and hence the algorithm will
return FAIL.
\QED

We will now show how to reduce the problem of finding benign revisions
to that of finding stable examples.  First we will define the notion
of example stability more precisely:

\begin{defn}
An example $E$ is {\bf stably covered} by a patchable theory
$\tup{\Gamma,\Omega}$ if, for every theory $\Gamma'$ obtainable from
$\Gamma$, $\Gamma'(E)=T$.  Similarly, $E$ is {\bf stably uncovered} by
$\tup{\Gamma,\Omega}$ if for every obtainable theory $\Gamma'$,
$\Gamma'(E)=F$.  $E$ is {\bf stable} in $\tup{\Gamma,\Omega}$ if it is
either stably covered or stably uncovered by $\tup{\Gamma,\Omega}$.
\end{defn}


We may now define the stability problem as follows.

\begin{defn}
The {\bf propositional stability problem} PSTABLE$(\Gamma,\Omega,E)$ is:
\begin{description}
\item[Given:] a patchable theory $\tup{\Gamma,\Omega}$ and an
example $E$ for $\Gamma$,
\item[Determine:] if $E$ is stably covered or stably uncovered by
$\tup{\Gamma,\Omega}$, returning $T$ if $E$ is stably covered, $F$ if
$E$ is stably uncovered, and $U$ otherwise.
\end{description}
\end{defn}

Then we have that:

\begin{theorem}
Given a patchable propositional theory $\tup{\Gamma,\Omega}$, some
distinguished component $c\in\Omega$, and a training set of labeled
examples ${\cal E}$, PBENIGN is polynomially reducible to PSTABLE.
\label{thm:benign-stable}
\end{theorem}

\proof
We prove the theorem by giving an algorithm which constructs a benign
repair.  
The algorithm works in two stages.  First, we find two subsets of 
$\E$: a set of {\bf obstructive} examples $O$, which are the examples for which 
$c$ must be
disabled; and a set of {\bf protected} examples $P$, which are the 
examples for which $c$ must not be disabled.
Next, using the assumption that our revision function is unrestricted, we 
construct a revision to $c$ which
disables $c$ for the examples in $O$ but not for those in $P$. 

\algorithm{PBENIGN}{$\Gamma,\Omega,c,\E$}
\begin{enumerate}\itemsep=0cm
\item $O\gets\emptyset,P\gets\emptyset$;
\item For each $\tup{E,l}\in\E$:
 \begin{enumerate}\itemsep=0cm
\item If \call{PSTABLE}{$\Gamma,\Omega\BS\{c\},E$}$=\neg l$,
	then $O\gets{O\cup\{E\}}$;
\item If \call{PSTABLE}{$\Gamma\BS\{c\},\Omega\BS\{c\},E$}$=\neg l$,
	then $P\gets{P\cup\{E\}}$;
 \end{enumerate}
\item If $O\cap{P}\neq\emptyset$, return FAIL;
\item Else:
 \begin{enumerate}\itemsep=0cm
 \item If $c$ is an antecedent literal, then:
  \begin{enumerate}\itemsep=0cm
  \item If $P=\emptyset$, return the revision that deletes $c$;
  \item Else, if $O=\emptyset$, return the null revision;
  \item Else, return FAIL;
  \end{enumerate}
 \item Else, return a revision with disabling set $D$ such that
	$O\subset{D}$ and $P\cap{D}=\emptyset$.
 \end{enumerate}
\end{enumerate}
Now, it is easy to see that if $O$ and $P$ are not disjoint, then 
$\tup{\Gamma,\Omega}$ is not repairable for $\E$, since in such a case 
at least one example exists which $\tup{\Gamma,\Omega}$ stably 
classifies incorrectly.  Conversely, if $\tup{\Gamma,\Omega}$ is not 
repairable for $\E$, there will be at least one example which is 
stably classified incorrectly, and that example will show up in both 
$O$ and $P$.  Hence, the failure condition is satisfied.

\def\hGO{\tup{\hat{\Gamma},\hat\Omega}}
\def\hG{\hat{\Gamma}}
\def\hO{\hat{\Omega}}
\def\hD{\hat{D}}
\def\he{\hat{E}}
\def\hE{\hat{\E}}
\def\hp{\hat{p}}
\def\hc{\hat{c}}
\def\hr{\hat{r}}
\def\hR{\hat{\R}}
\def\hl{\hat{l}}

Now suppose that $\tup{\Gamma,\Omega}$ is repairable for $\E$.  We
show that the patchable theory $\hGO=\tup{r(c,\Gamma),\Omega\BS\{c\}}$
is repairable, and hence $r$ is benign.  Consider now the stability of
examples in $\hGO$:
\begin{itemize}
\item $\hGO$ does not stably classify any example $E\in O$ incorrectly,
since $c$ is disabled for $E$ in $\hGO$, and $E\not\in P$ hence
\call{PSTABLE}{$\Gamma\BS\{c\},\Omega\BS\{c\},E$}$\neq\neg l$. 
\item $\hGO$ does not stably classify any example $E\in P$ incorrectly,
since $c$ is not disabled for $E$ in $\hGO$, and 
$E\not\in{O}$ hence
\call{PSTABLE}{$\Gamma,\Omega\BS\{c\},E$}$\neq\neg l$.
\item $\hGO$ does not stably classify any example $E\in\E\BS(P\cup{O})$
incorrectly, since regardless of whether or not $c$ is disabled for $E$, both
\call{PSTABLE}{$\Gamma\BS\{c\},\Omega\BS\{c\},E$}$\neq\neg l$, and
\call{PSTABLE}{$\Gamma,\Omega\BS\{c\},E$}$\neq\neg l$
hold.
\end{itemize}
Since $\hGO$ therefore does not stably classify any example incorrectly, it is
repairable, and hence $r$ is benign.
\QED

We now close the circle by proving the equivalence of PPATCH and
PSTABLE: 
\begin{cor}
PPATCH and PSTABLE can each be reduced to the other in polynomial time.
\label{cor:patch-stable}
\end{cor}
\proof
That PPATCH can be reduced to PSTABLE in polynomial time follows
directly from Theorems~\ref{thm:patch-benign} and
\ref{thm:benign-stable}.  In the other direction,
PSTABLE($\Gamma,\Omega,E$) trivially reduces to
PPATCH($\Gamma,\Omega,\{\tup{E,l}\}$) where $l=\neg\Gamma(E)$, by
noting that $\tup{\Gamma,\Omega}$ is repairable for $\{\tup{E,l}\}$ if
and only if $E$ is not stable in $\tup{\Gamma,\Omega}$.
\QED

\subsection{Determining example stability}
\label{sec:stability}

Given the results of the previous section, we see that theory patching
is tractable if and only if determining example stability is
tractable.  The question addressed in this section is: When is PSTABLE
(and hence PPATCH) tractable?  Intuitively, determining stability is
intractable if revisions to a component may both permit new proofs and
restrict old ones.  Determining the stability of an example (hence its
need to be repaired) may then require considering all possible
combinations of components which could be revised, leading to a
combinatorial explosion.  We therefore consider here a monotonicity
condition on theories, which requires that revising a component in the
theory either permits proofs or restricts proofs, but not both.  For
example, in a propositional theory without negation, literals
contribute solely towards preventing proofs, while clauses contribute
solely towards facilitating them.  We call a theory with such a
monotonicity condition {\it parity-definite}, as defined below.

More precisely, we define the parity of each component in a theory as
either {\it even}, {\it odd}, or {\it undefined}, as follows.
\begin{defn}
Given a propositional domain theory, define the {\bf parity} of its
root proposition to be {\em even}.  Further, recursively define the {\bf
parity} of:
\begin{itemize}
\item a clause to be {\em even} ({\em odd}) if the parity of its head
proposition is {\em odd} ({\em even}), and to be undefined otherwise;
\item an antecedent literal to a clause to be {\em even} ({\em odd}) if the
parity of its clause is {\em odd} ({\em even}), and to be undefined
otherwise;
\item an internal proposition to be {\em even} ({\em odd}) if every positive
antecedent literal for that proposition is {\em even} ({\em odd}), and
every negative antecedent literal containing that proposition is {\em odd}
({\em even}), and to be undefined otherwise.
\end{itemize}
\end{defn}

In general, odd components play the same role in a given theory as do
clauses in negation-free theories, in that they only facilitate proofs
of the root proposition in the theory, while even components play the
role of antecedent literals, as they only restrict such proofs.  Thus,
revisions to odd components have the effect of specializing the
theory, while revisions to even components have the effect of
generalizing the theory.  A theory that has only components with
defined parity, therefore, will be monotonic in the sense discussed
above.  Hence we define:

\begin{defn}
A domain theory is {\bf parity-definite} if every non-primitive 
component in the theory has a defined parity (even or odd).
\end{defn}

Note that we exclude primitive propositions from consideration, since
only the parity of components that may in principle be revised is
important.  This fact is highlighted by the following extension of the
definition of `parity-definite' to patchable theories:

\begin{defn}
A patchable domain theory $\tup{\Gamma,\Omega}$ is {\bf
parity-definite} if every component in $\Omega$ has a defined parity.
\end{defn}


The restriction to parity-definite theories is syntactic, rather than
semantic, since any theory may be reduced to an equivalent
parity-definite theory.  This is easily seen by reducing a theory to
a DNF formula containing only primitive propositions; the
`flat' theory corresponding to such a formula is parity-definite.
Thus, the restriction to parity definite theories takes on its primary
significance when not all components of a theory are open.

We now have that theory patching of parity-definite patchable
propositional theories is tractable:

\begin{theorem}[Propositional tractability]
PPATCH$(\Gamma,\Omega,\E)$ for parity-definite patchable theories
$\tup{\Gamma,\Omega}$ is solvable in time polynomial in $|\Omega|$ and
$|\cal E|$.
\label{thm:prop-tractability}
\end{theorem}

This theorem follows immediately from Corollary~\ref{cor:patch-stable}
and the following lemma.

\begin{lemma}
If $\tup{\Gamma,\Omega}$ is parity-definite,
PSTABLE$(\Gamma,\Omega,E)$ is 
solvable in time linear in $|\Gamma|$.
\label{lem:prop-stability}
\end{lemma}
\proof
Let $\opens_E\subset\Omega$ be the set of the open even components of
$\Gamma$, and $\opens_O\subset\Omega$ be the set of the open odd
components of $\Gamma$.  Note that $\Omega=\Omega_E\cup\Omega_O$.  Now
let $\Gamma_{\hbox{gen}}$ be the theory which results from deleting
the components in $\opens_E$ from $\Gamma$, and let
$\Gamma_{\hbox{spec}}$ be the theory which results from deleting the
components in $\opens_O$ from $\Gamma$.  Since deleting components in
$\opens_O$ from $\Gamma$ can only make it harder to prove an example,
an example is stably covered in $\Gamma$ if and only if it is covered
in $\Gamma_{\hbox{spec}}$.  Similarly, an example is stably uncovered
in $\Gamma$ if and only if it is uncovered in $\Gamma_{\hbox{gen}}$.
This gives the following linear algorithm for determining example
stability:

\algorithm{PSTABLE}{$\Gamma,\Omega,E$}
\begin{enumerate}
\item $\Omega_E\gets\{c\in\Omega\mid \hbox{$c$ even in $\Gamma$}\}$;
\item $\Omega_O\gets\{c\in\Omega\mid \hbox{$c$ odd in $\Gamma$}\}$;
\item $\Gamma_{\hbox{gen}}\gets\Gamma\BS\Omega_E$;
\item $\Gamma_{\hbox{spec}}\gets\Gamma\BS\Omega_O$;
\item If $\Gamma_{\hbox{gen}}(E)=\Gamma_{\hbox{spec}}(E)=T$, then return $T$,
\item Else if $\Gamma_{\hbox{gen}}(E)=\Gamma_{\hbox{spec}}(E)=F$, then return $F$,
\item Else return $U$.
\QED
\end{enumerate}


For example, 
applying the algorithm to the cup theory above gives us the theories
$\Gamma_{\hbox{gen}}$ and $\Gamma_{\hbox{spec}}$ shown in
Figure~\ref{fig:MPT-MRT}.  The example \{HAS-BOTTOM, LIGHT-WEIGHT,
HAS-CONCAVITY, UPWARD-CONCAVITY\} is easily seen to be stably
uncovered, as it is uncovered in both of these theories.  On the other
hand, the example \{HAS-BOTTOM, LIGHT-WEIGHT, HAS-CONCAVITY,
UPWARD-CONCAVITY, SMALL, DRY\} is not stable, since it is covered in 
$\Gamma_{\hbox{gen}}$ but uncovered in $\Gamma_{\hbox{spec}}$.

\begin{figure}[t]
\center
\begin{tabular}{|c|}
\hline
$\Gamma_{\hbox{gen}}$ \\
\begin{tabular}{lcl}
CUP	& $\leftarrow$ & UPRIGHT \And LIFTABLE \And OPEN \\
UPRIGHT	& $\leftarrow$ & HAS-BOTTOM \\ % \And FLAT-BOTTOM \\
LIFTABLE& $\leftarrow$ & GRASPABLE \And LIGHT-WEIGHT \\
OPEN	& $\leftarrow$ & HAS-CONCAVITY \And UPWARD-CONCAVITY \\
OPEN	& $\leftarrow$ & HAS-STRAW \\
GRASPABLE & $\leftarrow$ & HAS-HANDLE \\
GRASPABLE & $\leftarrow$ & SMALL \And DRY\\
\end{tabular}\\
\hline
\hline
$\Gamma_{\hbox{spec}}$ \\
\begin{tabular}{lcl}
CUP	& $\leftarrow$ & UPRIGHT \And LIFTABLE \And OPEN \\
UPRIGHT	& $\leftarrow$ & HAS-BOTTOM \\ % \And FLAT-BOTTOM \\
LIFTABLE& $\leftarrow$ & GRASPABLE \And LIGHT-WEIGHT \\
OPEN	& $\leftarrow$ & HAS-CONCAVITY \And UPWARD-CONCAVITY \\
OPEN	& $\leftarrow$ & HAS-STRAW \\
GRASPABLE & $\leftarrow$ & SMALL \And CERAMIC \And DRY\\
\end{tabular}\\
\hline
\end{tabular}
\caption{Theories generated in computing PSTABLE for the cup 
theory.\label{fig:MPT-MRT}}
\end{figure}

\subsection{Soundness and Completeness}
\label{sec:soundness}

In this section we will show how the concepts of benign repair and
example stability can be used in the analysis of soundness and
completeness of theory patching algorithms.  We consider here also
algorithms that operate under restricted revision functions.

Any theory patching algorithm, \IE, one that revises a given theory by
patching individual open components of the theory, may be cast in the
form of the following algorithm schema:

\algorithm{Revise}{$\Gamma,\Omega,\rho,\E$}
\begin{enumerate}
\item $\Gamma'\gets\Gamma$;
\item While {\bf termination-condition} does not hold:
\begin{enumerate}
\item Choose a component $c\in\Omega$;
\item Choose a revision $r\in\rho(c)$;
\item $\Gamma'\gets r(\Gamma')$;
\item $\R\gets\R\cup\{r\}$;
\end{enumerate}
\item Either return $\R$ or FAIL.
\end{enumerate}

A theory patching algorithm is {\bf sound} if whenever the algorithm
terminates it either returns a revision sequence $\R$ which repairs
$\tup{\Gamma,\Omega}$ for $\E$, or it returns FAIL and
$\tup{\Gamma,\Omega}$ is not repairable for $\E$.  The soundness of a
theory patching algorithm depends directly on whether certain of the
revisions it performs are benign:
\begin{theorem}[Propositional soundness]
A theory patching algorithm is sound if and only if (a) the {\it last}
revision it performs to each component $c$ is benign and (b) the
algorithm returns FAIL only when no such benign revision exists.
\label{thm:soundness}
\end{theorem}
\proof
Suppose a given theory patching algorithm terminates and the last
revision it performs to each component $c$ is benign.  Then, by the
argument given in the proof of Theorem~\ref{thm:prop-tractability},
the final revised theory $\Gamma'$ is repairable for $\E$.  On the
other hand, if the algorithm returns FAIL, by assumption no benign
repair exists for some component $c$, and so $\Gamma$ is not
repairable.  Hence the algorithm is sound.

Now suppose the given algorithm is sound and terminates for input
$\tup{\Gamma,\Omega}$.  Let $\Gamma'$ be the final revised theory in
computed by the algorithm, and let $\tup{\hG,\hO}$ be the patchable
theory obtained prior to the last revision $r^*$ to $c$.  Then
$\tup{r^*(c,\hG),\hO\BS\{c\}}$ is repairable since $\Gamma'$ can be
obtained from it by a sequence of permissible revisions.  Thus $r^*$
is benign.
\QED

Note that if the termination condition of a given theory patching
algorithm is guaranteed to eventually obtain for every $\Gamma$,
$\Omega$, and $\E$, the algorithm is also complete, in the sense that
it is guaranteed to return a revision sequence $\R$ that repairs
$\Gamma$ for $\E$, if one exists, and FAIL otherwise.

The difficulty of proving soundness and completeness of theory
patching under a restricted revision function stems from the fact that
in such cases it is difficult to find benign revisions.  However, in
the unrestricted case, we have a straightforward method for
determining soundness and completeness.  Recall the definitions of
{\it obstructive} and {\it protected} from the proof of
Theorem~\ref{thm:benign-stable}.

\begin{theorem}
For the case of unrestricted revisions, a theory patching algorithm
which always terminates is sound and complete if and only if the last
revision it performs to each component $c$ disables $c$ for every
obstructive example at $c$ and does not disable $c$ for any protected
example at $c$.
\label{thm:unrestrict-soundness}
\end{theorem}
\proof
This theorem follows directly from Theorem~\ref{thm:soundness} and the
proof of Theorem~\ref{thm:benign-stable}.
\QED

For parity-definite theories this condition is easily checked.  Two
theory patching algorithms that operate on parity-definite theories
with unrestricted revision are PTR \cite{PTR-jair} and EITHER and its
variants \cite{neither94,either94}.  The PTR algorithm uses a
probabilistic heuristic to decide where to repair such that later
revisions to a component are stronger than earlier revisions and the
last revision to a component is guaranteed to be benign
\cite{PTR-jair}.  PTR can thus easily be shown to be sound and
complete.

The EITHER algorithm patches theories without negation by first
finding a subset of leaf antecedent literals (the {\bf antecedent
cover}) and a subset of leaf clauses (the {\bf rule cover}) such that
revisions to the two covers will suffice to repair the theory for the
training set.  Each component in each cover is revised once.  The
revision performed to a component ensures that (a) the component is
disabled for all obstructive examples and that (b) the component is
not disabled for any currently correctly classified example.  Note,
however, that (b) is weaker than the required condition of ensuring
that the component is not disabled for any protected example, since
(b) ignores incorrectly classified examples which are nevertheless
protected.  Thus, the heuristic argument in favor of the convergence
of EITHER given by Ourston~\citeyear{phd:ourston} can only be
formalized provided that condition (b) is equivalent to the required
condition.  This is the case only if all the components in the
antecedent cover are revised first, and only then is the rule cover
computed and its constituent rules revised.  This constraint can
easily be removed if revisions are chosen that satisfy the condition
given in Theorem~\ref{thm:unrestrict-soundness}.

\section{First-Order Theory Patching}
\label{sec:first-order}

\subsection{Defining the problem}

We now extend our treatment to cover the problem of theory patching
for first-order theories.  In this section, we consider first-order
domain theories which are non-recursive, function-free, definite-clause
theories with a single root predicate $R(x_1,\ldots,x_n)$, and
negation-as-failure in clause antecedents.  We assume as given a set
of {\bf fact predicates}, where a theory may contain {\bf facts} each
of which is a (possibly partial) instantiation of the parameters
of a fact predicate in a bodiless clause.  Facts with no free
parameters are termed {\bf ground facts}.  For example, if $F(x,y)$ is
a fact predicate, the fact $F(1,2)$ is ground, while the fact $F(x,4)$
is non-ground.  A fact predicate cannot appear as the head of
a clause with a non-empty body. 

An {\bf example} $E$ for a first-order theory $\Gamma$ with root
$R(x_1,\ldots,x_n)$ is an assignment of the values $E^1,\ldots,E^n$ to
the respective parameters $x_1,\ldots,x_n$.  If $R(E^1,\ldots,E^n)$ is
proved in $\Gamma$, $E$ is termed {\bf covered} by $\Gamma$ (denoted
$\Gamma(E)=T$), otherwise $E$ is termed {\bf uncovered} by $\Gamma$
(denoted $\Gamma(E)=F$).  A {\bf labeled example} is a pair
$\tup{E,l}$ consisting of an example $E$ and a truth assignment
$l\in\{T,F\}$ for the instantiated root predicate $R(E^1,\ldots,E^n)$.
If $l=T$, the labeled example is termed {\bf positive}, otherwise it
is termed {\bf negative}.

The {\bf components} of a first-order theory are its clauses,
predicates, and the literals in the antecedent of each clause.

We now consider revisions to a first-order domain theory.  As in the
propositional case, we must first define what constitutes a revision
to a component as opposed to a global revision to the theory.

\begin{itemize}
\item
We regard deletion of a component to be a revision to that component.
Thus we can revise a clause or an antecedent literal by simply
deleting it from the theory.  Note that we can think of deleting an
antecedent literal as treating the literal as if it were always true.
Hence, we naturally extend the definition to propositions by defining
deletion of a non-primitive predicate $P(x_1,\ldots,x_n)$ to mean the
addition of a clause asserting that $P(x_1,\ldots,x_n)$ is true for
all instantiations of $x_1,\ldots,x_n$.  We denote the theory
resulting from the deletion of component $c$ from $\Gamma$ as
$\Gamma\BS\{c\}$.

\item
We may also revise a clause with head $P(x_1,\ldots,x_n)$ by adding a
new positive or negative literal for new predicate $Q(y_1,\ldots,y_k)$
to the body of the clause, and adding a set of new clauses defining
$Q$ to $\Gamma$.  In order to keep the effects of the revision local
to the clause under revision, we require that neither $Q$ nor any of
the predicates appearing in its definition are non-fact predicates in
$\Gamma$, and that $\{y_1,\ldots,y_k\}\subset\{x_1,\ldots,x_n\}$.

\item
Similarly, we may revise a predicate $P(x_1,\ldots,x_n)$ 
by adding a clause $C$ with 
head $P(x_1,\ldots,x_n)$ to $\Gamma$ along with a set of new clauses defining the literals in the body of $C$.  
In order
to keep the effects of the revision local to the predicate under revision, 
we require that the body of no clause added to 
$\Gamma$ contains a non-fact predicate in $\Gamma$.  
\end{itemize}

In the case of a revision to a clause with head $P(x_1,\ldots,x_n)$,
the set of instantiations to the variable vector
$\tup{x_1,\ldots,x_n}$ for which the new antecedent literal is false
is termed the {\bf disabling set} of the revision.  Similarly, in the
case of a revision to a predicate $P(x_1,\ldots,x_n)$, the set of
instantiations to $\tup{x_1,\ldots,x_n}$ for which the body of the new
clause is satisfied is termed the {\bf disabling set} of the revision.


As in the propositional case, the defining property of a revision at a
component is the set of instantiations for which the component is
disabled.  Note, however, that in the first order case, the disabling
set of a revision to a component consists of instantiations for the
variable vector appearing at {\it that} component.  Thus a revision
cannot be directly tailored to disable the component for individual
examples, which are instantiations of the variable vector at the root.

Note that some of the more exotic revisions considered in the
literature, such as changing the order of the variables in an
antecedent literal, are not revisions to individual theory components
as defined.  They can, however, be constructed as combinations of
revisions to individual components of the theory.

\begin{defn}
A {\bf patchable first-order theory} is a pair $\tup{\Gamma,\Omega}$
consisting of a first-order domain theory $\Gamma$ and a set $\Omega$
of components of $\Gamma$.  We call $\Omega$ the {\bf open components}
of $\tup{\Gamma,\Omega}$.
\end{defn}

A {\bf revision function} $\rho$ and the notion of {\bf
$\rho$-obtainability} are defined as in the propositional case.  We
say that $\rho$ is {\bf locally unrestricted}\footnote{We use the term
`{\it locally} unrestricted' to suggest that only the effect of a
revision on a local instantiation is determined directly; the effect
of a revision on an 
example (an instantiation to the root's variable vector) depends
globally on the structure of the theory.}  if for each open predicate
or clause component $c\in\Omega$ and set $\cal I$ of instantiations of
$c$'s variable vector\footnote{The variable vector of a clause is the
variable vector of the clause's head.}  there exists $r\in\rho(c)$
with disabling set $\cal I$.

Now we can define the first-order theory patching problem as in the
propositional case.

\begin{defn}
The {\bf first-order theory patching problem}
FPATCH$(\Gamma,\Omega,\rho,\E)$ is:
\begin{description}
\item[Given:] a patchable first-order theory $\tup{\Gamma,\Omega}$ and a
set $\E$ of labeled examples for $\Gamma$, 
\item[Find:] a theory $\Gamma'$, $\rho$-obtainable from $\Gamma$, such
that for all  
$E\in\E$, $\Gamma'(E)=l$, if such exists; otherwise return FAIL.
\end{description}
\end{defn}
If such a $\rho$-obtainable theory $\Gamma'$ exists, we say that
$\tup{\Gamma,\Omega}$ is {\bf repairable} under $\rho$ for $\cal E$.

This definition is exactly parallel to that of the PPATCH patching
problem for propositional theories, except that we consider
first-order theories.  FPATCH is considerably harder than PPATCH,
however, as we will see in the next section.  The restriction to
parity-definite theories (defined exactly as in the propositional
case) is not sufficient to ensure tractability, and the problem is
intractable even in quite restricted settings.

\subsection{Hardness}
\label{sec:1o-hardness}
\def\zero{{\sf Zero}}
\def\one{{\sf One}}

We consider in this section two restrictions on first-order domain
theories, showing that even with these restrictions, the patching 
problem is quite difficult.
A {\bf completely bound} theory is one in which every variable appearing in
an antecedent also appears in the head of that antecedent's clause.
A {\bf quasi-propositional} theory is a completely-bound theory in
which every literal in the theory has the same variable vector as the
root.

For example, the following theory is completely bound but not
quasi-propositional:
\begin{verbatim}
R(x,y,z) :- Q(x,y) & S(y,z)
Q(x,y)   :- T(x)
Q(x,y)   :- T(y) & S(y,x)
\end{verbatim}
The following theory is quasi-propositional:
\begin{verbatim}
R(x,y,z) :- Q(x,y,z) & S(x,y,z)
Q(x,y,z) :- T(x,y,z)
Q(x,y,z) :- T(x,y,z) & S(x,y,z)
\end{verbatim}
However, the following theory is not quasi-propositional (since the
order of the parameters changes):
\begin{verbatim}
R(x,y,z) :- Q(x,y,z) & S(x,y,z)
Q(x,y,z) :- T(y,x,z)
Q(x,y,z) :- T(x,y,z) & S(z,y,x)
\end{verbatim}

\begin{theorem}[First-order hardness I]
For any fixed revision function $\rho$ which allows deletion, 
FPATCH$(\Gamma,\Omega,\rho,\E)$ is NP-hard, even if we consider only
domain theories which:
\begin{itemize}
\item are negation free (hence parity-definite),
\item are completely bound,
\item are of bounded depth, 
\item contain no open clauses or propositions (only antecedent
literals are
open), and 
\item contain no non-ground facts.
\end{itemize}
\label{thm:first-hardness-1}
\end{theorem}
\proof
We prove the theorem by showing a reduction from the NP-complete
problem MONOTONE-SAT \cite{garey-johnson}.  Consider the monotone CNF
expression $A$ over the set of variables $V = \{x_i\}$
\[
  A = \bigwedge_i (\bigvee_j p_{ij}) \wedge \bigwedge_k (\bigvee_\l \neg 
q_{k\l})
\]
(where for all $i,j$ $p_{ij}\in{V}$ and for all $k,\l$,
$q_{k\l}\in{V}$).  We now construct a patchable theory
$\tup{\Gamma,\Omega}$ and associated set of examples $\cal E$ such
that the expression can be satisfied only if $\Gamma$ is repairable
for $\cal E$, under any $\rho$ which allows deletion.

Let the root of $\Gamma$ be the predicate $R$, whose parameters are
all the variables in $V$, plus a new variable $w$.  Let $\Gamma$ be a
theory as follows:
\[
\begin{array}{rcl}
R(x_1,\ldots,x_n,w)	&\IF& S(x_1,\ldots,x_n,w) \wedge
				T(x_1,\ldots,x_n,w)\\
	&&\\
	S(x_1,\ldots,x_n,w)	&\IF& \zero(w) \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_1(x_1) \wedge \zero(x_1) \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_2(x_2) \wedge \zero(x_2) \\
		& \vdots & \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_n(x_n) \wedge \zero(x_n) \\
	&&\\

T(x_1,\ldots,x_n,w)	&\IF& \one(w) \\
T(x_1,\ldots,x_n,w)	&\IF& 	Q_1(x_1) \wedge\cdots\wedge Q_n(x_n)\\
	&&\\
	Q_1(x)	&\IF& \one(x) \\
	Q_2(x)	&\IF& \one(x) \\
		& \vdots & \\
	Q_n(x)	&\IF& \one(x) \\
	&&\\
	\zero(0). &&\\
	\one(1). &&\\
\end{array}
\]
Note that $|\Gamma|=O(N)$ and that $\Gamma$ is negation free, is
completely bound, has a depth of 3, and contains only ground facts.

Let the set of open components $\Omega$ be the set of all the
antecedent literals to the clauses $Q_i(x)\IF \one(x)$.
Let $\rho$ be any revision function allowing deletion of the components in $\Omega$.

Let $\E$ be a set consisting of one labeled example for each conjunct
in $A$, as follows.  For each positive conjunct
$C_i=(\bigvee_j{p_{ij}})$, we construct a negative labeled example for
$R$, where the parameters $p_{ij}$ and $w$ are set to 0 and all other
parameters take on the value 1.  Similarly, for each negative conjunct
$C_k=(\bigvee_\l\neg{q_{k\l}})$, we construct a positive labeled
example for $R$, where parameters $q_{k\l}$ are set to 0 and all other
parameters (including $w$) are set to 1.

Now consider the patching problem FPATCH($\Gamma,\Omega,\rho,\E$).
Any permissible revision to $\Gamma$ consists of deleting some set of
antecedent literals of the form $\one(x_i)$ from clauses
$Q(x_i)\IF{\one(x_i)}$.  We now claim that any revision to $\Gamma$
which satisfies the examples determines a satisfying assignment
$\sigma$ to $V$, where if the revision deletes antecedent literal
$\one(x_i)$ from $\Gamma$, $\sigma$ assigns $x_i$ to TRUE, and
otherwise assigns it to FALSE.  Conversely, any such satisfying
assignment determines a satisfying revision, hence if no satisfying
revision exists, $A$ is unsatisfiable.

We now show that a revision satisfies an example $E_i\in\E$ if and
only if the corresponding truth assignment for $V$ satisfies the
example's corresponding conjunct $C_i$.  This suffices to establish
the theorem, since all examples in $\E$ must be satisfied
simultaneously.  Let $\Gamma'$ be the revised version of $\Gamma$,
where $\sigma$ is the substitution corresponding to the revision.

Consider first an arbitrary positive conjunct in $A$,
$C_p=\bigvee_j{x_{i_j}}$, whose corresponding negative example $E_p$
assigns each $x_{i_j}$ and $w$ to 0, and all other parameters to 1.
The only way for the example not to be covered by $\Gamma'$ is for $T$
to be unprovable for $E$ in $\Gamma'$.  This can only be the case if
at least one of the literals $Q_{i_j}(0)$ is unprovable, and hence the
antecedent literal to the corresponding clause in $\Gamma'$ is unrevised from
$\Gamma$.  This is the case exactly when $\sigma$ satisfies $C_p$.

Similarly, consider the negative conjunct $C_n=\bigvee_j\neg{x_{i_j}}$,
with corresponding positive example $E$ assigning each $x_{i_j}$ to 0,
and all other parameters (including $w$) to 1.
The only way for $E$ to be covered by $\Gamma'$ is if $S$ is proved
for $E$, which can only occur if some $Q_{i_j}(0)$ is proved, and
hence the antecedent literal to the corresponding clause has been revised.
This is the case exactly when $\sigma$ satisfies $C_n$.
\QED

Next we show that if we drop the restriction on non-ground facts (keeping all
other restrictions), FPATCH is hard even for quasi-propositional theories.

\begin{theorem}[First-order hardness II]
For any fixed revision function $\rho$ allowing deletion, FPATCH$(\Gamma,\Omega,\rho,E)$ is 
NP-hard, even if we only consider theories which: 
\begin{itemize}
\item are negation-free (hence parity-definite),
\item are of bounded depth, 
\item contain no open clauses or propositions (only antecedent literals 
are open), and 
\item are quasi-propositional (hence completely bound).
\end{itemize}
\label{thm:first-hardness-2}
\end{theorem}
\proof
Note that here we explicitly allow for non-ground facts.
We prove the theorem, as above, by showing a reduction from
MONOTONE-SAT \cite{garey-johnson}.  Take as given a monotone CNF
expression $A$ over the set of variables $V = \{x_i\}$
\[
  A = \bigwedge_i (\bigvee_j p_{ij}) \wedge \bigwedge_k (\bigvee_\l \neg 
q_{k\l})
\]
(where for all $i,j$ $p_{ij}\in{V}$ and for all $k,\l$,
$q_{k\l}\in{V}$).  We now construct a patchable theory
$\tup{\Gamma,\Omega}$ and associated set of examples $\cal E$ such
that $A$ can be satisfied only if $\Gamma$ is repairable
for $\cal E$, under any revision function $\rho$ which allows deletion.

Let the root of $\Gamma$ be the predicate $R$, whose parameters are
all the variables in $V$, plus a new variable $w$.  Let $\Gamma$ be a
theory as follows:
\[
\begin{array}{rcl}
R(x_1,\ldots,x_n,w)	&\IF& S(x_1,\ldots,x_n,w) \wedge
				T(x_1,\ldots,x_n,w)\\
	&&\\
	S(x_1,\ldots,x_n,w)	&\IF& \zero_w(x_1,\ldots,x_n,w) \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_1(x_1,\ldots,x_n,w) \wedge
					\zero_1(x_1,\ldots,x_n,w) \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_2(x_1,\ldots,x_n,w) \wedge
					\zero_2(x_1,\ldots,x_n,w) \\
		& \vdots & \\
	S(x_1,\ldots,x_n,w)	&\IF&  Q_n(x_1,\ldots,x_n,w) \wedge
					\zero_n(x_1,\ldots,x_n,w) \\
	&&\\
 
T(x_1,\ldots,x_n,w)	&\IF& \one_w(x_1,\ldots,x_n,w) \\
T(x_1,\ldots,x_n,w)	&\IF& 	Q_1(x_1,\ldots,x_n,w)
				\wedge\cdots\wedge Q_n(x_1,\ldots,x_n,w)\\
	&&\\
	Q_1(x_1,\ldots,x_n,w)	&\IF& \one_1(x_1,\ldots,x_n,w) \\
	Q_2(x_1,\ldots,x_n,w)	&\IF& \one_2(x_1,\ldots,x_n,w) \\
		& \vdots & \\
	Q_n(x_1,\ldots,x_n,w)	&\IF& \one_n(x_1,\ldots,x_n,w) \\
\end{array}
\]
\[
\begin{array}{lcl}
\zero_1(0,x_2,x_3,\ldots,x_n,w). &\hskip1cm& \one_1(1,x_2,x_3,\ldots,x_n,w).\\
\zero_2(x_1,0,x_3,\ldots,x_n,w). && \one_2(x_1,1,x_3,\ldots,x_n,w).\\
\vdots	&& \vdots \\
\zero_n(x_1\ldots,x_{n-1},0,w). && \one_n(x_1\ldots,x_{n-1},1,w). \\
\zero_w(x_1,\ldots,x_{n-1},x_n,0). && \one_w(x_1,\ldots,x_{n-1},x_n,1). \\
\end{array}
\]
Note that $|\Gamma|=O(N)$ where $N$ is the number of literals in $A$, and that 
$\Gamma$ is negation free, is
quasi-propositional (hence completely-bound), and has a depth of 3.

Let the set of open components $\Omega$ be the set of all the
antecedent literals to the clauses
$Q_i(x_1,\ldots,x_n,w)\IF\one_i(x_1,\ldots,x_n,w)$.
Let $\rho$ be any revision function allowing deletion of the components in $\Omega$.

Let $\E$ be a set consisting of one labeled example for each conjunct
in $A$, as follows.  For each positive conjunct
$C_i=(\bigvee_j{p_{ij}})$, we construct a negative labeled example for
$R$, where the parameters $p_{ij}$ and $w$ are set to 0 and all other
parameters take on the value 1.  Similarly, for each negative conjunct
$C_k=(\bigvee_\l\neg{q_{k\l}})$, we construct a positive labeled
example for $R$, where parameters $q_{k\l}$ are set to 0 and all other
parameters (including $w$) are set to 1.

An argument isomorphic to that given in the proof of
Theorem~\ref{thm:first-hardness-1} gives that $A$ can be satisfied
only if FPATCH($\Gamma,\Omega,\rho,\E$) is solvable, \IE,
$\tup{\Gamma,\Omega}$ is repairable for $\cal E$.
\QED

Note that the constructions given above can be modified easily to replace the restriction 
of bounded theory depth with a restriction of bounded theory width.

\subsection{Tractability}

In the previous section we showed that FPATCH (for restricted and unrestricted revision 
functions) is intractable even if
we severely restrict the class of theories considered such that, in
addition to being negation-free, of bounded depth, and with all open
components 
antecedent literals, theories either (a) contain no non-ground facts {\bf or}
(b) are quasi-propositional.  We now show that FPATCH with locally unrestricted revisions 
is tractable for
parity-definite theories for which {\bf both} (a) and (b) hold, even
without the other restrictions.

As in the propositional case, we drop the $\rho$ when talking about FPATCH under locally 
unrestricted revision functions.

\begin{theorem}[First-order tractability]
For locally unrestricted revision functions, \\
FPATCH$(\Gamma,\Omega,\E)$ for parity-definite quasi-propositional
theories with no non-ground facts is solvable in time polynomial in
$|\Omega|$ and $|\E|$.
\label{thm:first-tractability}
\end{theorem}
This theorem is actually quite weak, since the restrictions allow a
straightforward reduction to the propositional case.

\proof
The reduction to PPATCH is as follows.
\begin{itemize}
\item Let $\hG$ be the propositional theory
obtained from $\Gamma$ by replacing each literal $P(x_1,\cdots,x_n)$
by the proposition $\hp$.  

\item Let $\hO$ consist of the components of
$\hG$ which correspond to the components in $\Omega$.  

\item Let the primitive propositions of $\hG$ be those which
correspond to literals for fact predicates in $\Gamma$.

\item For any labeled example $\tup{E,l}$, let
the corresponding propositional labeled example, $\tup{\he,\hl}$, be
such that $\he$ is a truth assignment to the primitive propositions of
$\hG$ such that for each $\hp$, $\he(\hp)=T$ if and only if
$P(E^1,\cdots,E^n)$ is a ground fact in $\Gamma$, and $\hl=l$.  Also,
for any set of labeled examples $\E$, let $\hE$ be the corresponding
set of propositional labeled examples.

\item For a propositional repair $\hr$ on propositional component
$\hc\in\hG$ with disabling set $\hD$, the corresponding first-order
revision $r$ on first-order component $c\in\Gamma$ is defined as the
revision with disabling set $D$.
\end{itemize}

It then follows that any sequence of revisions $\hR=\{\hr_i\}$ that solves 
PPATCH($\hG,\hO,\hE$) yields a corresponding sequence 
of revisions $\R=\{r_i\}$ 
which solves FPATCH($\Gamma,\Omega,\E$).  Moreover, if no positive solution 
exists for PPATCH($\hG,\hO,\hE$) then none exists for 
FPATCH($\Gamma,\Omega,\E$).
\QED


\subsection{Discussion}

How do our results in first-order relate to the propositional case?
In the propositional case, we saw that sufficient conditions for
tractability of theory patching were (a) that the theory be
parity-definite, and (b) that the revision function be unrestricted.
In the first-order case, however, we see that local unrestrictedness
is a much weaker condition than having unrestricted revisions in the
propositional case.  This is because a revision of a component in
first-order only affects the instantiations of the component's
variable vector and does not directly affect examples, \IE,
instantiations of the root's variable vector.  In fact, the additional
conditions for tractability imposed above on the structure of the
theory implicitly constitute a stronger unrestrictedness condition,
which can be made explicit as follows.

A revision function $\rho$ on a theory $\Gamma$ is {\bf truly
unrestricted} if $\rho$ and $\Gamma$ are such that given an open
clause or predicate component in $\Gamma$ and any two disjoint sets of
{\it examples} $A$ and $B$, a revision exists which can disable the
component for every example in $A$ without disabling the component for
any example in $B$.  This condition fails if, for instance, two
different examples agree on all the variables appearing at the
component, or if a predicate appears more than once in the theory each
time with a different variable vector, so that the predicate cannot be
revised for one example without affecting other examples.  Having
truly unrestricted revisions makes the problem tractable for
parity-definite theories, since the effect of a revision may be
evaluated locally at a single component, without requiring
consideration of other possible revisions at other components.



\section{Conclusions}

In this paper we have developed some necessary and some sufficient
conditions for the soundness and tractability of theory patching.  We
have thus addressed the problem of theory revision in general, without
restricting our focus to any particular algorithm.  The central notion
in theory patching is that of the benign revision, \IE, that any
non-retractable revision must ensure the repairability of the
resulting theory.  Since benign revisions must rule out stably
misclassified examples, the key to theory patching is determining
example stability.  In fact, the two problems, theory patching and
determining stability, are polynomially equivalent.  In general, the
patching problem is hard, but we have found that theory patching is
tractable if the input theory is parity-definite (\IE, monotonic with
respect to revision) and revisions are truly unrestricted (\IE, any
open component can be disabled for an arbitrary set of input
examples).  Moreover, we have shown how the soundness of a theory
revision method can be checked by verifying that certain of the
revisions it performs are benign.

We have shown how to find {\it some} hypothesis obtainable from the
input theory which is consistent with the given training examples, but
we have not considered here the quality of the hypothesis obtained, in
terms of convergence to some target concept (say, in the PAC learning
framework \cite{valiant84}).  It is worth noting that the very
condition of truly unrestricted revisions, which we have shown is
useful for ensuring that patching is tractable, leads to difficulty in
learnability, since the hypothesis space is then very large.  In fact,
in the truly unrestricted case, the VC-dimension of the hypothesis
space may be as large as the total number of possible examples, since
the set of truly unrestricted revisions at a component shatters
arbitrary sets of examples at that component.  Thus the question of
what conditions are required for convergence of theory patching to a
target theory remains open.

\acks{We would like to thank William Cohen and the anonymous reviewers
for their comments on previous drafts of this paper which helped
improve it greatly.  We would also like to thank Rina Schwartz for her
comments on an earlier draft of this paper.}


\bibliography{/u/segel/argamon/lib/bib/learning,/u/segel/argamon/lib/bib/mapping,/u/segel/argamon/lib/bib/revise}
\end{document}
