SATEN: An Object-Oriented Web-Based Revision and Extraction Engine
Mary-Anne Williams and Aidan Sims
Business Technology Research Laboratory
NSW 2308
Australia
nmr3.tex
\documentstyle[aaai209]{article}

\begin{document}

\title{SATEN: An Object-Oriented Web-Based Revision and Extraction Engine}
\author{Mary-Anne Williams and Aidan Sims\\
Business Technology Research Laboratory\\ 
University of Newcastle
\\ NSW 2308, Australia 
\\ maryanne@cafe.newcastle.edu.au \ \ \ \ \ \ \ \ \ aidan@math.newcastle.edu.au 
 }
\maketitle

\section{General Information}


SATEN\footnote{SATEN a Sagacious Agent for Theory Extraction and revisioN is available at  http://cafe.newcastle.edu.au/saten} is an object-oriented web-based extraction and belief revision engine. It runs on any computer 
via a Java 1.1 enabled browser such as Netscape 4. SATEN performs belief revision based on the AGM approach \cite{agm}.  The extraction and belief revision reasoning engines operate on a user specified ranking of information. One of the features of SATEN is that it can be used to integrate mutually inconsistent commensuate rankings into a consistent ranking.


\section{General Description of the System} 


SATEN has two reasoning engines:  a revision engine and an extraction engine. Both engines operate on a user-specified ranking of information.
 
The process of {\sl extraction} involves the recovery of a consistent ranking from an inconsistent ranking. Several strategies are available for this process. Extraction can be seen as a generalisation of Brewka's work on subtheories \cite{Brewka}. It is also related to Poole's work \cite{Poole,Dubois}. 

{\sl Revision} models the incorporation of new information (a belief) into a knowledge base.  The main difficulty in modeling this process is that the incoming information may be inconsistent with the agent's knowledge base. Consequently, the agent must determine the information to be relinquished before the new information can be accepted, if the agent is to maintain a consistent knowledge base. There are several constructive definitions of belief revision based on various preference relations over the agents knowledge. These preference relations attempt to capture the relative importance of information with respect to change. When an agent is forced to give up beliefs in order to accept some new information then, if presented with a choice, a response would be to choose to retain more important information, like system laws and integrity constraints, rather than contingent facts and default facts. 

\vskip 8pt
\noindent 
SATEN is capable of: 
\begin{itemize}
 \item Theory Extraction
 \item Iterated Belief Revision 
  \item Nonmonotonic Reasoning 
 \item Possibilistic Reasoning 
 \item Hypothetical Reasoning
\end{itemize}

Using combinations of these capabilities SATEN can perform information integration/fusion on mutually inconsistent commensurate knowledge bases and can calculate
Spohnian reasons \cite{SpohnB}. 

SATEN currently implements the  reasoning strategies below based on  a user specified ranking of beliefs (logical formulae). A {\em ranking} can be specified as mapping from beliefs to [1,2,3,...] in which case the most important information is given the lowest rank, i.e. rank is inversely proportional to importance. Alternatively, beliefs can be ranked using {\em degrees of belief} between 0 and 1 - the higher the degree the more important the information, in particular tautologies are assigned 1, whilst inconsistencies and nonbeliefs are given 0. SATEN can derive an ordinal ranking from a set of specified degrees automatically, by toggling one of the  menu settings.

\begin{itemize}
\item Standard Adjustment \cite{JELIA,IJCAI95,KR94} is based on the standard epistemic entrenchment construction \cite{gm} for Belief Revision. 
\item Maxi-Adjustment is based on maximal inertia \cite{IJCAI97}. Maxi-adjustment proceeds from the top of the ranking and moves down it rank by rank. At each rank it deletes all the beliefs that are inconsistent with other beliefs at that rank and above.
\item Hybrid Adjustment is a combination of standard adjustment and maxi-adjustment \cite{IJCAI97}. Adjustment is computationally ``easier" than maxi-adjustment, however the main shortcoming of adjustment is that it maintains beliefs only if there is an \emph{explicit reason to keep them}, whilst maxi-adjustment removes beliefs only if there is an \emph{explicit reason to remove them}. Hybrid adjustment performs an adjustment which computes  the core beliefs to be retained, and then it performs a maxi-adjustment which is used to regather as many  beliefs  as possible that were discarded during the adjustment phase.
 \item Global Adjustment is similar to a maxi-adjustment except that it takes all beliefs in the ranking into consideration when computing the minimally inconsistent  subsets, instead of proceeding rank by rank. It removes the least ranked beliefs "causing" the inconsistency.
\item Linear Adjustment is similar to maxi-adjustment except that it removes all the beliefs at ranks which contain incosisitencies with beliefs above them \cite{Nebel}. IF there is only one belief at each rank, then linear and maxi-adjustment are identical.
\item Quick Adjustment is identical to maxi-adjustment except that rather
than removing all beliefs it randomly chooses a minimal number of beliefs from each set of
inconsistent beliefs in this way the inconsistency is removed.
 \end{itemize}

 A number of examples are available via a dropdown menu which highlight the different behaviour of the strategies.



\section{Methodology}

An inherent difficulty that arises when trying to model world states using the predicate calculus is that of consistency. Under the rules of formal logic, anything is derivable from a contradiction, hence it is imperative that consistency of the model be maintained at all times so that the agent acting on that model is able to make sound decisions. However, it is not uncommon in the realm of belief-based reasoning for newly acquired information to be inconsistent with the current set of beliefs. For instance, suppose that an agent believes that {\sl Tweety is a bird,} and that {\sl all birds can fly.} This agent subsequently discovers that, {\sl Tweety is a penguin,} and knowing that {\sl penguins can't fly,} will now have to deal with the fact that this new information is inconsistent with what it already believes.

It is clear that when this sort of situation arises, the agent will need to select a set of beliefs to be removed from its knowledge base in order to maintain consistency in its knowledge base when the new belief is inserted, thus allowing it to continue to reason on the basis of its revised knowledge base. However, the question arises: which beliefs should be removed? Even in the above example, the removal of any subset of the beliefs listed will make the new information that {\sl Tweety is a penguin} consistent, so the question of which belief or set of beliefs to remove has no clear answer.

Alchourr\'on, G\"ardenfors and Makinson \cite{agm,AMa,AMb} investigated a set of rationality postulates regarding theory change operators. These postulates appear to capture much of what is required of an ideal rational system of theory change. In particular, they developed three primary classes of theory change operators: expansion, contraction and revision. Expansions are deterministic, and can be expressed set-theoretically, but it is well known that the logical properties of a body of information are not strong enough to uniquely determine a revision or contraction operator. Consequently, some sort of preference order needs to be imposed on the beliefs in the agent's knowledge base. This approach to Belief Revision has come to be known as the AGM paradigm.

Two common models used to impose the preference order required by the AGM paradigm on systems of beliefs are {\sl epistemic entrenchment orderings} \cite{gm} and {\sl systems of spheres} \cite{Grove}. An epistemic entrenchment ordering ranks the sentences in the knowledge base, whereas a system of spheres is a total preorder of the set of possible world states. SATEN uses the epistemic entrenchment representation and uses the services of a full first order theorem prover implemented in Java \cite{VADER}. Revision of a system of spheres can be implemented  
via a standard Database Management System \cite {IIS}.

The implementation of revision in SATEN is steeped in the AGM paradigm \cite{agm}.
G\"ardenfors and Makinson's \cite{gm} showed that an epistemic entrenchment can uniquely determine how an agent will react to the pressures of impinging information. Their construction is an elegant theoretical result, and to use it as the foundation for a computer-based implementation of belief revision the following problems need to be addressed. 

\begin{itemize}
\item
Epistemic entrenchments order all the beliefs in the underlying language. The underlying language may be infinite in size, therefore a finite representation for an epistemic entrenchment is required. 

\item A new knowledge base, rather than a new epistemic entrenchment ordering is constructed. However from a practical point of view developing a new entrenchment ranking is imperative because an implementation must have the capacity to perform iterated revision. 

\end{itemize}

An implementation of belief revision must propagate  an epistemic entrenchment ordering (or more precisely its finite representation).  
SATEN overcomes the first problem using a finite partial entrenchment ranking \cite {JELIA,IJCAI97} as the underlying representation scheme, and it overcomes the second problem using transmutations \cite{Spohn,KR94,IJCAI97}. 


%The agm paradigm requires that the knowledge base to be operated upon be a {\sl theory}. That is, it is required to be closed under the logical entailment operator, $\vdash$. However, the logical closure of even a single sentence is prohibitively large even for modest size languages, so it is necessary, in order to implement belief revision on a computer, to work only with {\sl theory bases}; that is, finite sets of beliefs whose theory closure is the agent's current theory. Williams \cite{JELIA} developed {\sl ensconcements} to facilitate such an implementation. Another problem involved in implementations of Belief Revision is that standard operators on entrenchments do not produce another entrenchment, but rather simply a revised theory. Since a reasoning agent using belief revision would need to iterate the process, it is necessary to incorporate the production of a new entrenchment into the revision operator. Williams \cite{KR94} developed transmutations to address this problem, and SATEN implements a number of Belief Revision strategies  based on this approach and on the work in \cite{IJCAI95,IJCAI97}.

%\subsection{The agm Paradigm}
%The agm paradigm is a  formal approach to information change; it provides a mechanism for the revision and contraction of information. The rationality postulates set forth in \cite{agm} are intended to embody the principle of {\sl  minimal change}, which is the metaprinciple behind all theory change operators. The goal is to ensure that the change in the knowledge base incurred by a revision or contraction operation is, in some sense, minimal. Though rationality postulates are necessary only in the case of revision and contraction operators, the agm paradigm actually specifies an expansion operator as well, and we will present the definitions of all three.


%\subsection{Languages, Theories and Theory Bases}
%The agm paradigm does not insist on the predicate calculus as its underlying language. In fact, it only requires: 
%\begin{itemize}
%\item
%some countable language $L$ that is closed under a complete set of boolean connectives (complete in the sense that they can be used to express any two variable truth function); and 
%\item 
%a logic on $L$ whose consequence relation $\vdash$ satisfies a set of requirements \cite[\S2]{JELIA} which ensure that it is sufficiently well-behaved. 
%\end{itemize}
%In particular, the predicate calculus with the standard notion of entailment does the job, and this is the case we have in mind throughout.

%If $S$ is a set of sentences in $L$, we refer to the logical closure of $S$ as $Cn(S)$, by which we mean the set of logical consequences of $S$ or equivalently, the set of all sentences $\alpha$ in $L$ which satisfy $S \vdash \alpha$. A {\sl theory} of $L$ is any subset $T$ that is closed under $\vdash$, that is, $Cn(T) = T$. We denote by $\mathcal{T}_L$ the set of all theories of $L$. A {\sl theory base} for a theory $T$ is any set $\Gamma \subseteq L$ of statements satisfying $Cn(\Gamma) = T$. If $\Gamma$ has finitely many elements, we refer to it as a {\sl finite theory base} for $T$. We say that a theory $T$ is {\sl finitely axiomatizable} if it has a finite theory base.


%\subsection{agm Expansion}
%The agm paradigm treats theories in the language $L$ as information states, so that an operation on the current information state (or knowledge base) is described by a transformation on the corresponding theory \cite{JELIA}. \cite{agm} defines the {\sl expansion} of a theory $T$ by a formula $\alpha$ by $T^{+}_{\alpha} := Cn(T \cup \{\alpha\})$. That is to say, the expansion of $T$ by $\alpha$ is the set of all things that follow logically from $T$ and $\alpha$, or equivalently, the smallest theory of $L$ containing both $T$ and $\alpha$. One should note that "contraction is a monotonic operation" \cite{JELIA}, meaning that if $\beta$ is in $T$ then $\beta$ is also in $T^{+}_{\alpha}$ irrespective of $\alpha$. In particular, this means that if $\neg\alpha\in T$ then $T^{+}_{\alpha}$ is inconsistent.


% 1. Is there a general methodology as to how to encode a problem,
%    to take advantage of your work?                                    
% 2. If there is no general methodology, is it likely to be developed in
%    the near future? 






%\subsection{agm Contraction}
%By contrast to the relatively simple definition of the expansion operator, contraction and revision are not uniquely determined by the current theory and the sentence with respect to which the theory is to be modified. Consequently, they "cannot be represented logically and set theoretically." \cite{JELIA}. Thus, instead of defining specific operations as was done in the case of expansion, the agm paradigm describes a class of operators for contraction and revision operators.

%A contraction of a theory is essentially some operation that removes some element $\alpha$ from the theory $T$. More formally, it involves the removal of some set $S_{\alpha}$ of sentences from $T$ so that the remaining portion of $T$ does not logically entail $\alpha$: that is, $\alpha \not\in Cn(T\setminus S_\alpha)$. \cite{agm} defines a {\sl contraction operator} $^-$ to be any function from $\mathcal{T}_L \times L$ to $\mathcal{T}_L$ written $(T,\alpha) \mapsto T^-_\alpha$ which satisfies the following eight postulates for any $\alpha, \beta$ in $L$ and any $T$ in $\mathcal{T}_L$:
%\begin{description}
%\ item{$(^-1)$} $T^-_\alpha \in \mathcal{T}_L$: that is, the resulting set is a theory of $L$;
%\item{$(^-2)$} $T^-_\alpha \subseteq T$: that is, $^-$ really is a contraction --- it only removes things from $T$;
%\item{$(^-3)$} If $\alpha \not\in T$ then $T \subseteq T^-_\alpha$: that is, if $\alpha$ was not in the theory $T$ to begin with, then contracting with respect to $\alpha$ does nothing;
%\item{$(^-4)$} If $\not\vdash \alpha$ then $\alpha \not\in T^-_\alpha$: that is, provided $\alpha$ is not a tautology, $\alpha$ will not be in the contracted theory; the operator is guaranteed to remove $\alpha$ where possible;
%\item{$(^-5)$} If $\alpha\in T$ then $T \subseteq (T^-_\alpha)^+_\alpha$: that is, if we contract with respect to $\alpha$ and then expand with respect to $\alpha$, we recover our original theory;
%\item{$(^-6)$} If $\alpha\vdash\beta$ and $\beta\vdash\alpha$ then $T^-_\alpha = T^-_\beta$: that is, contracting with respect to equivalent formulae has the same effect.
%\item{$(^-7)$} $T^-_\alpha \cap T^-_\beta \subseteq T^-_{\alpha\wedge\beta}$: that is, contracting with a conjunction keeps at least all the things that are kept in contractions with both of the conjuncts; and
%\item{$(^-8)$} If $\alpha \not\in T^-_{\alpha\wedge\beta}$ then $T^-_{\alpha\wedge\beta} \subseteq %T^-_\alpha$: that is, if we must remove $\alpha$ in order to remove $\alpha\wedge\beta$ then we must remove everything else that would have been removed with $\alpha$ as well.
%\end{description}

%Of the above postulates, $(^-1)$ - $(^-4)$ and $(^-6)$ are self-explanatory. Postulate $(^-5)$, known as {\sl recovery}, is the most debated of the axioms, and much work has been done regarding operators that don't satisfy this requirement. Postulates $(^-7)$ and $(^-8)$ govern the behaviour of contractions with respect to conjunctions, and ensure that we don't throw away too much when removing a conjunction as compared to simply removing the conjuncts.


%\subsection{agm revision}
%Similarly to the contractions, a revision of a theory is the process of changing the theory so as to incorporate some new belief whilst maintaining the consistency of the theory. Naturally, this may involve the removal of some of the beliefs currently in the theory. Formally, a {\sl revision operator} is a function $^*$ from $\mathcal{T}_L \times L$ to $\mathcal{T}_L$ written $(T,\alpha) \mapsto T^*_\alpha$ which satisfies the following eight postulates for any $\alpha, \beta$ in $L$ and any $T$ in $\mathcal{T}_L$:
%\begin{description}
%\item{$(^*1)$} $T^*_\alpha \in \mathcal{T}_L$: that is, the resulting set is a theory of $L$;
%\item{$(^*2)$} $\alpha \in T^*_\alpha$: that is, the revision does insert the required belief;
%\item{$(^*3)$} $T^*_\alpha \subseteq T^+_\alpha$: that is, $^*$ inserts nothing extraneous;
%\item{$(^*4)$} If $\neg\alpha \not\in T$ then $T^+_\alpha \subseteq T^*_\alpha$: that is, if $\alpha$ was consistent with the theory $T$ to begin with, then revision with $\alpha$ is just expansion with $\alpha$;
%\item{$(^*5)$} $T^*_\alpha = \perp$ if and only if $\vdash \neg\alpha$: that is, the revises theory is inconsistent if and only if $\alpha$ itself is a contradiction;
%\item{$(^*6)$} If $\alpha\vdash\beta$ and $\beta\vdash\alpha$ then $T^*_\alpha = T^*_\beta$: that is, revising with respect to equivalent formulae has the same effect.
%\item{$(^*7)$} $T^*_{\alpha\wedge\beta} \subseteq (T^*_\alpha)^+_\beta$: that is, revising with a conjunction keeps at least all the things that are kept in revisions with either of the conjuncts provided the conjuncts are consistent; and
%\item{$(^*8)$} If $\neg\beta \not\in T^*_\alpha$ then $(T^*_\alpha)^+_\beta \subseteq T^*_{\alpha\wedge\beta}$: that is, if $\beta$ is consistent with the revision with $\alpha$, then revision with $\alpha\wedge\beta$ keeps at least as much as revision with respect to $\alpha$ does.
%\end{description}

%\subsection{The Relationship Between Contraction and Revision}
%The reader will have noted the similarity between the two sets of postulates for contraction and revision. In fact, in \cite{agm}, Alchourr\'on, G\"ardenfors and Makinson show that revision and contraction operators are interdefinable; specifically, they have shown that $(T^-_{\neg\alpha})^+_\alpha$ defines a revision operator (the {\sl Levi Identity}), and that $T \cap T^*_\alpha$ defines a contraction operator (the {\sl Harper Identity}).

%These two sets of postulates circumscribe the classes of theory operators permissible under the agm paradigm. In particular, the revision operators form the class of operators used in Belief Revision. Unfortunately, the postulates do not specify a unique operator given a theory and a belief with which to revise, and so some sort of additional structure needs to be imposed on the belief set so that a revision operator may be constructively defined. To achieve this, we turn to the next section and {\sl epistemic entrenchment orderings,} and to the following section and {\sl systems of spheres}.



%\section{Epistemic Entrenchment Orderings}
%As was seen in the previous section, the rationality postulates alone are insufficient to define a unique contraction or revision operator. In order to deal with this problem, we impose a total order on the set of beliefs in $L$. This ordering is intended to reflect the reluctance of an agent to give a given belief up, so that the tautologies are, perforce, ranked higher than any other belief, whilst the contradictions (and non-beliefs) are ranked lower than any other belief. Epistemic orderings \cite{Ga,gm} were developed to embody this idea, and can be used to determine a unique revision or contraction operator for a given entrenched theory. The definition is as follows: Given a theory $T$ of $L$, an {\sl epistemic entrenchment related to $T$} is any binary relation $\le$ on $L$ satisfying:
%\begin{description}
%\item{(EE1)} $\le$ is transitive;
%\item{(EE2)} for all $\alpha, \beta$ in $L$, if $\alpha\vdash\beta$ then $\alpha\le\beta$;
%\item{(EE3)} for all $\alpha, \beta$ in $L$, $\alpha\le\alpha\wedge\beta$ or $\beta\le\alpha\wedge\beta$;
%\item{(EE4)} When $T$ is consistent, $\alpha \not\in T$ if and only if $\alpha \le \beta$ for all $\beta$ in $T$;
%\item{(EE5)} If $\beta \le \alpha$ for all $\beta$ in $L$ then $\vdash\alpha$;
%\item{(EE6)} every nonempty set in $L$ has a minimal element under $\le$ (there are no infinitely descending chains); and
%\item{(EE7)} every nonempty set in $L$ has a maximal element under $\le$ (there are no infinitely ascending chains).
%\end{description}

%These axioms ensure that the ordering respects logical entailment (EE2, EE3) in that we believe in any statement at least as strongly as we believe in any statement that entails it (for example, if we were nearly certain that all birds had feathers, and equally certain that Tweety was a bird, it would be somewhat inconsistent for us to have too much doubt that Tweety had feathers). They also ensure that the ordering is well behaved (EE1), and that it is bounded below by the contradictions and non-beliefs (EE4) and bounded above by the tautologies (EE5).


%\subsection{Epistemic Entrenchments and Operators}
%In \cite{gmb}, G\"ardenfors and Makinson show that for every contraction operator $^-$ there is an epistemic entrenchment ordering $\le$ so that the condition ($E^-$) below is true for every $\alpha$ in $L$, and likewise that for every epistemic entrenchment ordering $\le$ the formula in condition ($E^-$) defines a contraction operator.
%\[
%(E^-) \hskip1.5cm T^-_\alpha = 
%\begin{cases}
%\beta\in T | \alpha < \alpha\vee\beta {\rm \ if\ }\alpha{\rm \ is\ not\ a\ tautology} \\
%T {\rm \ otherwise.}
%\end{cases}
%\]

%Consequently, using the notion of an epistemic entrenchment ordering, we
%are able to construct a unique contraction operator associated to every
%epistemically entrenched theory $T$ for a language $L$. The Levi Identity
%allows us to convert a contraction operator into a related revision
%operator, and Peppas and Williams \cite{PeppasWilliams} proves that this revision
%operator is given by: \[
%(E^*) \hskip1.5cm T^*_\alpha = 
%\begin{cases}
%\beta\in L | \neg\alpha < \neg\alpha\vee\beta {\rm\ if\ }\alpha{\rm\ is\ not\ a\ contradiction} \\
%\perp {\rm \ otherwise.}
%\end{cases}
%\]
%giving us a well-defined and unique revision operator associated to our epistemic entrenchment as required.



%\section{Systems of Spheres}
%Whereas the epistemic entrenchment construction of a unique theory change operator focuses on the specification of a contraction operator, the construction using a system of spheres gives rise explicitly to a revision operator, and it is necessary to use the Harper Identity to get a contraction operator from it. In order to define systems of spheres, we must adopt a little extra notation. Namely, we denote by $\Theta_L$ the set of {\sl consistent} theories of $L$, and given a set of formula, $\Delta$ we define $[\Delta]$ to be the set of all consistent, complete theories containing $\Delta$ \cite{PhD}. Now, if $T$ is in $\Theta_L$, \cite[\S3.2.3]{PhD} defines a system of spheres $\Sigma$ centered at $[T]$ to be any family of subsets of $\Theta_L$, each of which we call a {\sl sphere}, satisfying:
%\begin{description}
%\item{($\Sigma1$)} $\Sigma$ is totally ordered by set inclusion: given any two sets, one is included in the other;
%\item{($\Sigma2$)} $[T]$ is a $\subseteq$ minimal element: that is, $[T]$ is contained in every sphere;
%\item{($\Sigma3$)} $\Theta_L$ is a $\subseteq$ maximal element: every sphere is a subset of $\Theta_L$; and
%\item{($\Sigma4$)} For every formula $\alpha$, if there is any sphere in $\Sigma$ that intersects $[\alpha]$, then there is a smallest sphere in $\Sigma$ intersecting $[\alpha]$.
%\end{description}
%
%This last requirement ($\Sigma4$) will seem rather strange because it seems intuitive, but it is used to ensure that the subset ordering is well behaved. It does not hold true for every totally ordered collection of subsets: if we take our $T$ to be the open interval $(0,1)$ in the real numbers, and take our spheres to be of the form $(0,1+\epsilon)$ for all real numbers $\epsilon$, then there is no smallest interval containing $1$ (or even $(0,1]$), though every interval but $T$ itself does contain $1$ (respectively $(0,1]$). Note also that whilst ($\Sigma2$) and ($\Sigma3$) only specify maximal and minimal elements, ($\Sigma1$) ensures that the ordering is total, so that these minimal and maximal elements are unique --- they are actually the minimum and maximum elements.

%These are called systems of spheres because it is convenient to visualize them as such. Think of $T$ as the smallest of a group of concentric spheres, so that each new element essentially adds another `layer' to the previous one.


%\subsection{Systems of Spheres and Operators}
%Now we define two functions: for each $\alpha$ in $L$, define $C_\Sigma (\alpha)$ to be the smallest sphere in $\Sigma$ that intersects $[\alpha]$; and again for each $\alpha$ in $L$, define $f_\Sigma (\alpha)$ to be the intersection of $[\alpha]$ with $C_\Sigma (\alpha)$. That is, $f_\Sigma (\alpha) = [\alpha]\cap C_\Sigma (\alpha)$. Grove \cite{Grv}, developed a relationship between these systems of spheres and revision operators. The results link systems of spheres to revision operators via the following formula:
%\[
%(\Sigma^*) \hskip1.5cm T^*_\alpha = 
%\begin{cases}
%f_\Sigma (\alpha) { if }\neg\alpha{ is not a tautology}
%\perp { otherwise.}
%\end{cases}
%\]
%where by $\cap f_\Sigma (\alpha)$ we mean all formulae belonging to every theory that is in both $[\alpha]$ and $C_\Sigma (\alpha)$.

%Grove's results state that: a) for every system of spheres $\Sigma$ centered on $[T]$, there is a revision operator $^*$ for $T$ so that $(\Sigma^*)$ is true for every $\alpha$ in $L$; and b) for every revision operator $^*$ for $T$ there is a system of spheres $\Sigma$ centered at $[T]$ for which $(\Sigma^*)$ is true for every $\alpha$ in $L$.

%It is important to note, in this case, that for any given revision operator, there will be more than one system of spheres giving rise to it \cite{PhD}. However, each system of spheres clearly gives rise to a unique revision operator, so that Grove's approach does, in fact, allow us to construct a unique set of theory change operators for a theory as we required.


%\subsection{Specifics}
                                        
% 1. What is the significance of your system being logic-based? 
% 2. What is the semantics of your system (e.g. propositional logic,
%    first-order logic, default logic, stable or well-founded semantics, etc.)? 
% 3. Why is this an important feature of your work? 
% 4. How will your work influence other areas such as artificial
%    intelligence,  knowlege bases and deductive databases? 






%\section{Implementing Belief Revision}
%Lakemeyer says \cite{Lak} "it is widely accepted that agents, because of their limited resources, believe some, but by no means all of the logical consequences of their beliefs." Consequently, the study of theory change does not necessarily model the behaviour of intelligent agents, but rather of ideal rational systems. Makinson says \cite{Mak} that theory change is "essentially a mathematical exercise on an idealized,\dots elegant model." However, when theory change operators are applied to theory bases, they are syntactically dependent, and they fail to satisfy the agm recovery postulate $(^-5)$, causing many objections to such an endeavor.

%In response to the noncompliance with the recovery postulate, many including Williams \cite{JELIA} argues that recovery is inappropriate for a limited reasoning agent since it is as Makinson puts it "inextricably tied to the consequence relation." The problem of syntax dependence has been viewed by some as an indication that the beliefs in the theory base itself are held with greater commitment than are those merely derivable from the base. According to Rott \cite{Rotta}, "real life theories are generated from finite axiomatizations \dots the axioms may carry different epistemic weight. Both the syntactical encoding of a theory and the prioritization are held to be relevant for theory change." However, Williams \cite{PhD} proposes the endowment of theory bases with additional structure, an {\sl ensconcement ordering}, which associates an epistemic entrenchment ordering to the theory generated by the theory base. The question of recovery is addressed with a number of convincing arguments that its imposition can cause undesirable and counterintuitive results in a limited reasoning agent \cite{Han,Nie}, and implementations of belief revision do not, in general, require that the recovery postulate be satisfied.


%\subsection{Ensconcements}
%Williams' ensconcements \cite{PhD} are essentially the same as Rott's E-bases %\cite{Rottb} which he developed independently as a way to give a standard representation of an epistemic entrenchment. For $\alpha$ in $L$, and an epistemic entrenchment $(T,\le)$, Williams \cite{PhD} defines the {\sl cut} at $\alpha$, $cut_{\le}(\alpha)$ to be the set of formulae ranked at least as high as $\alpha$, that is, $\{\beta\in L | \alpha \le \beta\}$, and the {\sl proper cut} at $\alpha$, $cut_<(\alpha)$ to be all formulae ranked strictly higher than $\alpha$, that is, $\{\beta \in L | \alpha < \beta\}$. Williams then defines an entrenchment to be {\sl finitely representable} precisely when it has a finite number of natural partitions under $\le$ and every cut is finitely axiomatizable.

%An ensconcement is defined to be a set of formulae $\Gamma$ totally preordered by $\preceq$ such that $\preceq$ satisfies the following properties \cite{PhD}:
%\begin{description}
%\item{$(\preceq1)$} For all nontautological $\beta$ in $\Gamma$, $\beta$ is not entailed by the formulae ranked strictly higher than it; and
%\item{$(\preceq2)$} For all $\alpha \preceq \beta$ for every $\alpha$ in $\Gamma$ if and only if $\beta$ is a tautology.
%\end{description}

%If an ensconcement has a finite number of natural partitions, it is said to be a finite ensconcement. Note, however, that $\Gamma$ need not be finite in order for $(\Gamma, \preceq)$ to be a finite ensconcement. Williams defines, for each $\alpha$ in $L$, the cut at $\alpha$ in the ensconcement $(\Gamma, \preceq)$, $cut_\preceq(\alpha)$, to be the set of all formulae $\beta$ in $\Gamma$ with the property that the set of beliefs strictly more ensconced than $\beta$ does not entail $\alpha$. Intuitively, this is saying that $\alpha$'s implicit rank in the ensconcement is the lowest rank $\alpha$ could occupy without violating $(\preceq1)$. 


%\subsection{Entrenchments and Ensconcements}
%Williams  generates an entrenchment of $Cn(\Gamma)$ from $(\Gamma, \preceq)$ by defining $\alpha \le \beta$ if and only if $cut_\preceq(\beta) \subseteq cut_\preceq(\alpha)$ \cite{PhD}. That is, the ensconcement ordering is extended to an entrenchment ordering by allowing beliefs not explicitly contained in the ensconcement to occupy the lowest rank they can in the corresponding entrenchment without violating the entrenchment axioms. Williams shows that the entrenchment $(Cn(\Gamma), \le_\preceq)$ arising from $(\Gamma, \preceq)$ is finite if and only if the $(\Gamma, \preceq)$ is finite.

%Williams \cite{JELIA} gives algorithms for constructing a (unique) finite ensconcement from a given finite epistemic entrenchment, and likewise constructing a (unique) finite entrenchment from a finite ensconcement. \cite{JELIA} proceeds to give definitions of expansion, contraction and revision operators corresponding to a given ensconcement. The expansion operator is the intuitive one $\Gamma^\oplus_\alpha = \Gamma \cup \{\alpha\}$. The contraction and revision operators can be given explicitly, but Williams proves that these definitions are actually equivalent to the following intuitive definitions based on the standard theory change operators given by $(E^-)$ and $(E^*)$, where the epistemic entrenchment in question is that arising from the ensconcement:
%\begin{description}
%\item{$\Gamma^\ominus_\alpha$} = $(Cn(\Gamma))^-_\alpha \cap \Gamma$.
%\item{$\Gamma^\otimes_\alpha$} = $(Cn(\Gamma))^*_\alpha \cap %\Gamma^\oplus_\alpha$.
%\end{description}

%That is to say, we can define canonical revision and contraction operators on an ensconced theory base simply by the restriction of the canonical revision and contraction operators to the corresponding entrenched theories.



%\section{Transmutation}
%The theory change and theory base change operators described in previous sections all rely on a preference relation being given prior to revision or contraction. According to Williams \cite[\S5.0]{PhD}, "although this provides desirable theoretical freedom, it leads to difficulties in designing computer-based knowledge revision systems. In order to accommodate a subsequent theory change such a system would require guidance in determining a subsequent preference relation\dots hence the problem of iterated belief revision is determining how the underlying preference relation should change\dots"

%The ideas involved in formalizing these transmutations are rather complex, and revolve around sets of functions known as {\sl Ordinal Conditional Functions} (OCF's) \cite{Spohn}, {\sl Ordinal Nice Preoder Functions} (OPF's) \cite[\S5.3]{PhD}, and {\sl Ordinal Epistemic Entrenchment Functions} (OEF's) \cite[\S5.5]{PhD}. {\sl Transmutation} operators are used to transmute one OCF (or OPF or OEF) into another. These functions essentially assign to each formula in a knowledge base an ordinal, and the operators on the knowledge systems require as input not only a formula $\alpha$, but also an ordinal $i$ indicating the degree of acceptance $\alpha$ is to be accorded in the new knowledge base, where the significance of $i$ is its ranking of $\alpha$ in the original knowledge base with respect to its associated OCF, OPF or OEF. Conditionalizations \cite{Spohn} and adjustments \cite{PhD} are two classes of operators that act on these systems.

%Williams \cite{PhD} illustrates the theoretical details of the three classes of ordinal functions. She also investigates the connections between the three classes, showing that there exist transformations between each pair of classes that preserve the knowledge set and its dynamical properties in each case. Finally, she defines equivalence of operators amongst the three classes, and produces explicit conditions which relate the transmutations on OCF's, OPF's and OEF's, and demonstrates that both conditionalizations and adjustments satisfy these conditions. Since it has been shown that "any transmutation of a knowledge system in a finitary language can be achieved by a sequence of conditionalizations and adjustments, they provide a powerful mechanism for supporting the computer-based implementation of a knowledge system transmutation" \cite{PhD}.


%\subsection{Users and Useability} 
% 1. Must the potential user be an expert in logic or need to have a 
%    deep knowledge of the specific area of the application?
% 2. Is your system sufficiently flexible to handle other problems? 
% 2. If so, what kind of problems, and what would have to be done
%    to apply your system? 
% 3. Is your system applied outside your research group or even in other areas? 
% 4. Is it likely to be used in the future (are there concrete plans to do so)? 

%\section{Evaluating the System}

% MANDATORY

\section{Applying the System}
The user specifies a prioritised knowledge base. We have found that for most applications the user-specified ranking can be otained in a natural way during the analysis and design phase \cite{applications}. 

The following  guidelines for designing a ranking were developed in \cite{IJCAI97}:


\begin{itemize}
\item Important information should be made explicit in the ranking
\item Information should be represented in its simplest logical form
\item Maximize the number of ranks, and minimise the number of beliefs at each rank for better performance
\item Rankings should be as irredundant as possible
\item Subsumption at the same rank should be avoided
\item User specifies reasons 
\item Check the contraposition of reasons does not lead to undesired behaviour
\end{itemize}



SATEN can revise first order theory bases.
It uses the services a Java first order theorem prover VADER \cite{VADER} to determine consequence relations, and hence takes worst-case exponential time in the number of formulae in the knowledge base to compute even  propositional revision. However, given Horn input clauses, the system will use a Linear Descent algorithm for its deductions, resulting in linear time efficiency. A number of strategies have been implemented in this system : {\sl standard adjustment}, {\sl maxi-adjustment}, {\sl hybrid adjustment}, {\sl global adjustment}, {\sl linear adjustment}, and {\sl quick adjustment}.

Theory extraction is related to belief revision and uses an extraction operator is a map between epistemic entrenchment orderings which, given an inconsistent ranking, extracts from it some (in some sense) maximal consistent ranking/theory base. Whilst every extraction operator gives rise rather naturally to a corresponding revision operator, it remains unknown whether the converse is true. When SATEN performs a revision, the internal behaviour is  to add the new belief to the base at an appropriate rank, and then to perform a Theory Extraction, before normalising the beliefs to achieve the revised theory base. The process of normalisation converts any ranking into a partial entrenchment ranking.

SATEN is capable of performing both Belief Revision and Theory Extraction on theory bases, and of determining the degree of an arbitrary wff in it's theory base, and can {\sl normalize\/} a ranked theory base. It is also capable of automatically ranking the beliefs in the theory base --- the user has the option to view the total order as a ranking (with the (0,1)-values of the entrenchments suppressed) although the rankings are always represented internally with (0,1)-values. Finally, the user may specify whether new beliefs added to the base without a rank should, by default, be placed at the top of the ranking, or at the bottom. This feature can be used when the rank of new information is unknown. The most conservative approach would place the new information without rank at the both of the ranking.


\subsection{Input Format} SATEN accepts any Predicate Calculus wff's as
input.  Variables in the predicate calculus must begin with a capital
letter, and contain only alphanumeric symbols and underscores (\_).
Constants have the same format as variables, but must begin with a lower
case letter. Predicate and function names must comply with the same format
as variables and constants respectively, but must be followed by a
parenthesized list of arguments separated by commas. 

Input should be in fully parenthesised logic syntax and should not contain
spaces:

\begin{itemize} 
\item Negation is a minus sign (-).
\item Implication is an arrow composed of a minus sign and a greater than sign ($-\hskip -4pt >$). Note no space between the two symbols.
\item Conjunction is an ampersand (\&).
\item Disjunction is a pipe ($\vert$).
\item The universal quantifier is an asterisk (*).
\item The existential quantifier is an exclamation mark (!).
\item Constants must begin with lower-case letters.
\item Variables with upper-case letters.
\item Functions start with lower-case.
\item Propositional statements start with lower-case.
\item First Order Predicates begin with upper-case.
\end{itemize}

Expression grouping is with parentheses, as is function (and predicate) argument list demarkation. User input should not include any double underscores (\_\_) as these are used by the program to tag system-generated variables and skolem functions.
\vskip 6 pt

\noindent Example input format:
\vskip 3 pt
 *X(Psychopathic(X)$\vert$ Emotional(X))     

-null     

hopes\&dreams     

*X(!Y(Mother(X,Y))) 

 !Z(EatsChocolate(Z)$-\hskip -4pt >$Happy(Z))

 *Y(-Income(Y)$-\hskip -4pt >$-Loan(Y))

\hskip 12pt
We can encode "
``{\sl For all $X$ there exists a $Y$ such that $Y$ is the mother of $X$, and for all $Y$, if $Y$ is the daughter of Ben's maternal grandmother, then $Y$ is Ben's mother, or $Y$ is Ben's aunt.\/}'' using the following sentence: 

\[
(*X(!Y(M(X,Y)))\&(*Y(D(MGM(ben),Y) -\hskip -4pt > \]
\vskip -20pt
\[ \hskip 2cm (M(ben,Y)|A(ben,Y)))
\]
where $X$ and $Y$ are variables, $M(X,Y)$ is a predicate of two variables with name $M$, $MGM(X)$ is a function of one variable with name $MGM$, and $ben$ is a constant. 

\subsection{Strategies}
The {\sl standard adjustment} strategy finds the largest cut of the inputs to SATEN that is consistent with the incomming information, and keeps this as the result of the revision. This is quite fast, but removes alot of beliefs from the theory base in comparison to the other strategies because as shown in \cite{IJCAI97} the independence of beliefs must be explicitly specified in the ranking.

The {\sl maxi-adjustment} strategy looks at each individual rank in the belief set, and removes the union of all subsets $S$ of the beliefs on that rank having the properties
\begin{enumerate}
\item $S$ is inconsistent with the union of the incomming information and all the information ranked higher in the base than $S$; and
\item no proper subset of $S$ satisfies $1$.
\end{enumerate}

This strategy keeps many of the beliefs in the theory base, but is also quite slow as it has to examine all subsets of each rank. Performance is improved if the agent is more discerning. our algorithm is anytime \cite{IJCAI97} so the longer the agent has to revise the better the result.

The {\sl hybrid adjustment} strategy represents a combination of the standard adjustment and maxi-adjustment strategies. When revising with $a$, hybrid adjustment first finds every belief $b$ in the base such that $-a|b$ is in the base, and is at the same rank as $-a$ (this is the adjustment step --- it is removing every belief that ``explicitly" fails to be a consequence of the cut above $-a$), and then performs a maxi-adjustment on what is left. So in other words maxi-adjustment is used to recoup as much of the ranking as the time set aside for the revision permits.

This strategy is comparable to maxi-adjustment with regard to the number of beliefs retained, and though somewhat faster on average, has the same worst-case time expenditure as the maxi-adjustment procedure.

The {\sl global adjustment} strategy behaves exactly as maxi-adjustment does, but acting under the assumption that all beliefs have the same rank. This strategy is quite slow, and is not as parsimonious in what it removes as maxi-adjustment, but is highly intuitive with respect to the set of beliefs removed (without reference to their ranks). It comes as close as possible to eliminating the need for a ranking.

The {\sl linear adjustment} strategy \cite{Nebel}looks at the successive cuts of the theory-base and, at every rank at which the cut is inconsistent, removes the entire rank from the base. This is quite time-efficient, and keeps more beliefs in the base than standard adjustment, but, unlike hybrid adjustment and maxi-adjustment, is fairly ad-hoc about the beliefs to be kept in the theory base. 

The {\sl quick adjustment} strategy is an attempt to capture the judiciousness of maxi-adjustment without the associated time expenditure. Once a given rank of beliefs is discovered to cause a contradiction, quick adjustment begins adding beliefs from the left end of that rank until a contradiction is discovered. It then removes these beliefs, one at a time, keeping track of which ones eliminate the contradiction when they are removed. It is these ``culprit'' beliefs that are then removed from the theory base. This process is then iterated.
This strategy has the advantage of improving performance by reducing the
amount of processing
at each
rank, and also emulates the output of maxi-adjustment much of the time. However, its behaviour depends upon the order of the inputs on a given level of the theory base, and hence is somewhat ad hoc. The system could be easily extended to generate more than one ranking and used to perform credulous reasoning. Instead of randomly choosing an alternative, all alternative revised rankings could be created.

\subsection{Other Options} SATEN implements three additional (optional)
strategies that interact with the various Belief Revision strategies
outlined above. These strategies are {\sl subsumption removal,
recovery,\/} and {\sl nuclear revision.\/} Of these three, the second two
are appropriate with any belief revision strategy, but subsumption removal
cannot be used in conjunction with the standard adjustment strategy.
This is the only type of nuclear revision currently implemented. Other
approaches like attributing half-lifes to individual beliefs will be
available in the next version of SATEN.

Using {\sl subsumption removal\/} ensures that any strategy which must choose from a set of beliefs to remove will preferrentially remove beliefs that are subsumed by the incomming belief. For example, maxi-adjustment will look amongst the set of beliefs it was going to remove for the subset that are subsumed by the incomming belief. If there are none, it will proceed as before, but if there are some, it will throw them away first, and then check again for consistency. If the result is still not consistent, the maxi-adjustment algorithm is run again on the remaining beliefs.

The {\sl recovery\/} option ensures that the recovery postulate is satisfied by the revisions. This is achieved by, rather than removing a belief $b$, replacing it with the disjunction $b|a$ where $a$ is the new belief. The only time we do not do this is if $b|a$ is a tautology.

The concept of {\sl nuclear revision} models the fact that beliefs that are not constantly reinforced tend to become less substantial to an intelligent agent. When nuclear revision is enabled, the user will be asked for a half-life. This is the constant factor by which the entrenchment of every belief in the base drops after each operation on the theory base. Thus, if the half-life were set at $0\cdot5$, then the entrenchment of each belief in the theory base would be halved after each operation.


\subsection{Examples}
SATEN has a substantial example menu intended to indicate the correct input form for SATEN, and demonstrate SATEN's capabilities, but also to illustrate the differences between the various belief revision strategies that SATEN implements. These examples are broken into three categories: propositional, predicate, and contrast of strategies.

The first of these indicates the correct input and behaviour of SATEN when presented with propositional inputs only. Under these conditions, SATEN tends to be somewhat more efficient than in the predicate case for the reasons outlined in the VADER hyperbook in the section on performance issues.

The second set of examples indicate SATEN's behaviour with the more general input form of the Predicate Calculus, specifically, its behaviour when quantifiers and variables are involved. The differences are essentially at the theorem prover level, and are opaque to SATEN itself.

The third set of examples are designed to indicate differences in behaviour between the different revision strategies. This is done for two reasons: the first is to highlight the salient points that make each strategy desirable or undesirable in comparison to the others; the second, which is, to some degree subsumed by the first, is to demonstrate that there actually {\it is\/} a difference between each pair of strategies, and that these differences do not require overly sophisticated examples to demonstrate --- in particular, propositional calculus is sufficient, and it is possible to get pairwise distinct behaviour from the strategies on an example with just nine beliefs and four distinct ranks.

\bibliography{nmr2000}
\bibliographystyle{bibaaai}
 

\end{document}

nmr3.bbl
\begin{thebibliography}{}



\bibitem[\protect\citeauthoryear{Alchourr\'on \& Makinson}{82}]{AMa}
Alchourr\'on, C., and Makinson, D.
\newblock 1982.
\newblock On the Logic of Theory Change: Partial Meet Functions for Contraction
  and Revision.
\newblock {\em Theoria}  48: 14 -- 37.

\bibitem[\protect\citeauthoryear{Alchourr\'on \& Makinson}{85}]{AMb}
Alchourr\'on, C., and Makinson, D.
\newblock 1985.
\newblock On the Logic of Theory Change: Safe Contraction.
\newblock {\em Studia Logica}  44, 405 -- 422.




\bibitem[\protect\citeauthoryear{Brewka}{89}]{Brewka}
Brewka, G.
\newblock 1989.
\newblock Preferred Subtheories: An Extended Logical Framework for Default
  Reasoning.
\newblock In {\em International Joint Conference on Artificial Intelligence},
  1043 -- 1048.


\bibitem[\protect\citeauthoryear{Dubois et al}{94}]{Dubois}
{Dubois, D., Lang, J. and Prade,H.}
\newblock 1994.
\newblock Automated Reasoning using Possibilistic Logic.
\newblock {\em IEEE Transactions on Knowledge and Data Engineering}  6: 64 -71.


\bibitem[\protect\citeauthoryear{Alchourr\'on et al}{85}]{agm}
{Alchourr\'on, C., G\"ardenfors, P., and Makinson, D.}
\newblock 1985.
\newblock Two Modelings for Theory Change.
\newblock {\em Journal of Symbolic Logic}  50: 510--530.

\bibitem[\protect\citeauthoryear{G\"ardenfors \& Makinson}{88}]{gm}
{G\"ardenfors, P., and Makinson, D.}
\newblock 1988.
\newblock Revisions of Knowledge Systems using Epistemic Entrenchment.
\newblock In {\em Proceedings of the Second Conference on Theoretical Aspects
  of Reasoning about Knowledge},  83 -- 96.

\bibitem[\protect\citeauthoryear{Grove}{88}]{Grove}
{A., Grove}
\newblock 1988.
\newblock On the Logic of Theory Change: Contraction Functions and their Associated Revision Functions.
\newblock {\em Journal of Philosophical Logic}  17: 157 -- 170.


\bibitem[\protect\citeauthoryear{{Sims and Williams}}{97}]{VADER}
{Sims, A.D., and Williams, M-A.}
\newblock 1997.
\newblock VADER: A web-based first order theorem prover.
\newblock at http://cafe.newcastle.edu.au/vader.

\bibitem[\protect\citeauthoryear{Nebel}{94}]{Nebel}
Nebel, B.
\newblock 1994.
\newblock Base Revision Operations and Schemes: Semantics Representation, and
  Complexity.
\newblock In {\em European Conference on Artificial Intelligence}.
\newblock John Wiley and Sons.

\bibitem[\protect\citeauthoryear{Poole}{88}]{Poole}
Poole, D.
\newblock 1988.
\newblock A Logical Framework for Default Reasoning.
\newblock {\em Artificial Intelligence}  13: 81 -- 132.

\bibitem[\protect\citeauthoryear{Spohn}{83a}]{SpohnB}
Spohn, W.
\newblock 1983.
\newblock Deterministic and Probabilistic Reasons and Causes.
\newblock {\em Erkenntnis}  19: 371 -- 396.

\bibitem[\protect\citeauthoryear{Spohn}{88a}]{Spohn}
Spohn, W.
\newblock 1988.
\newblock Ordinal Conditional Functions: A Dynamic Theory of Epistemic States.
\newblock In {\em in Harper, W.L. and Skyrms, B. (eds), Causation in Decision,
  Belief Change, and Statistics II},  105--134.
\newblock Kluwver Academic Publishers.

\bibitem[\protect\citeauthoryear{Williams}{94a}]{JELIA}
Williams, M.-A.
\newblock 1994a.
\newblock On the Logic of Theory Base Change.
\newblock In {\em Logics in Artificial Intelligence, LNCS No 835},  86 -- 105.
\newblock Springer Verlag.

\bibitem[\protect\citeauthoryear{Williams}{94b}]{KR94}
Williams, M.-A.
\newblock 1994b.
\newblock Transmutations of Knowledge Systems.
\newblock In {\em Principles of Knowledge Representation and Reasoning:
  Proceedings of the Fourth International Conference},  619 -- 629.
\newblock Morgan Kaufmann, San Mateo, CA.

\bibitem[\protect\citeauthoryear{Williams}{95}]{IJCAI95}
Williams, M.-A.
\newblock 1995.
\newblock Iterated Theory Base Change: A Computational Model.
\newblock In {\em in the Proceedings of the Fourteenth International Joint
  Conference on Artificial Intelligence},  1541 -- 1550.
\newblock Morgan Kaufmann, San Mateo, CA.

\bibitem[\protect\citeauthoryear{Williams}{97a}]{IJCAI97}
Williams, M.-A.
\newblock 1997a.
\newblock Anytime Belief Revision.
\newblock In {\em in the Proceedings of the Fourteenth International Joint
  Conference on Artificial Intelligence},  74--79.
\newblock Morgan Kaufmann, San Mateo, CA.

\bibitem[\protect\citeauthoryear{Williams}{97b}]{IIS}
Williams, M.-A.
\newblock 1997b.
\newblock Belief Revision via Database Update.
\newblock In {\em in the Proceedings of the International Intelligent
  Information Systems Conference},  74--79.
\newblock IEEE Press.

\bibitem[\protect\citeauthoryear{Williams}{98}]{applications}
Williams, M.-A.
\newblock 1998.
\newblock Applications of Belief Revision.
\newblock In {\em Transactions and Change in Logic Databases, LNCS No 1472},  285 -- 314.
\newblock Springer Verlag.

\end{thebibliography}
