<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">


\documentclass[fleqn]{article}
\setlength{\textwidth}{12.2cm}
\setlength{\textheight}{19.3cm}
%\renewcommand{\theequation}{e.\arabic{equation}}
\newcommand{\fl}{\mbox{${\cal L}(FL)$}}                % Patrick's Lang
\newcommand{\sd}{\mbox{${\cal L}(SD)$}}                % Surface Lang
\newcommand{\limp}{\rightarrow}
\newcommand{\cs}{\gg}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\lang}{ {\cal L} }
\newcommand{\kbu}{\mbox{\em KBU}}
\newcommand{\lkbu}{\mbox{\em LKBU}}
\newcommand{\kbr}{\mbox{\em KBR}}
\newcommand{\KB}{\mbox{\em KB}}
\newcommand{\isval}{\hat{=}}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\sknot}{\neg}
\newcommand{\skand}{\wedge}
\newcommand{\skor}{\vee}
\newcommand{\skcond}{\rightarrow}
\newcommand{\skbicond}{\leftrightarrow}
\renewcommand{\land}{\wedge}           %logical and
\renewcommand{\lor}{\vee}              %logical or
\renewcommand{\lnot}{\neg}             %logical negation
\newcommand{\lcond}{\rightarrow}           %logical material implication
\newcommand{\lbicond}{\leftrightarrow}           %logical material bicond
\newcommand {\pud} {\mbox {$[\!]$}}
\newcommand{\nl}{\hspace{2cm}\\ \rm}
\newcommand{\koniec}{\rule{0.08in}{0.08in}}
\newcommand{\dcirc}{\mbox{$CIRC_D(T)$}}
\newcommand{\prent}{\mbox{$|\!\!\approx_{stl}$}}
\newcommand{\symdiff}{\mbox{$\stackrel{.}{-}$}}
\newcommand{\act}{$A_1,\ldots,A_n$}
\def\Proof{\noindent\underline{Proof}\hspace*{3mm}\mbox{ }}
\def\implies{\Rightarrow}
\def\subst{\leftarrow}
\def\lequ{\equiv}
\def\wtt{\Leftrightarrow}
\def\impl{\Rightarrow}

\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{remark}{Remark}[section]
\newtheorem{tw}{Theorem}
\newtheorem{note}{Note-to-remove}[section]
\newtheorem{ex}{Example}
\newtheorem{alg}{Algorithm}
\newtheorem{proposition}[prop]{Proposition}

\pagestyle{empty}
\begin{document}

\title{\bf Lazy Knowledge Base Update}
\author{        Witold \L ukaszewicz and
      Ewa Madali\'{n}ska-Bugaj \thanks{The authors were partially supported by the Wallenberg Foundation and
by KBN grant  T 11C 009 19.} ~ \\
        { Institute of Informatics,} 
        { Warsaw University} \\
        { Warsaw, Poland }}
\date{}

\maketitle
\thispagestyle{empty}
\begin{abstract}
Knowledge base update has been given much attention in the AI literature. 
The best-known solution to this problem is
Winslett's PMA formalism.
In this paper we propose   different intuitions standing behind 
  knowledge base update.
 Roughly speaking, we consider an  update formula $\alpha$
not as an effect of an action to be performed, but rather as an
observation about dynamically changing world made by an agent.
This observation, if it is consistent with the knowledge base,
is assumed to be just a new piece of information about the world.
Otherwise, it is assumed that a {\em single} action has been performed and
$\alpha$ is its, usually partial, effect. 

We formalize our approach using Dijkstra's semantics. We also
examine the properties of our update operator with respect to
Katsuno and Mendelzon's postulates.


\end{abstract}

\section{Introduction}

There are two kinds of modifications of a knowledge base
that have been given much attention 
in the AI literature: {\em knowledge base revision} 
and {\em knowledge base update}.

Knowledge base revision, (\kbr{}, for short)
 \cite{agm85,Nebel89}
is formulated as follows. We are given a knowledge base $KB$,
representing a static world, and a 
formula $\alpha$ representing
new information. Our task is to determine  the resulting knowledge base,
$KB*\alpha$. The crucial point is that $KB$ can contain incorrect
information, so that $\alpha$ may be inconsistent with $KB$\footnote{In this case, it is assumed that 
$\alpha$ is more reliable than $KB$.}.
The theoretical foundations of \kbr{} have been formulated in
\cite{agm85} by means of {\em rationality postulates}, referred 
 as the
AGM postulates.    


Knowledge base update (\kbu \, for short) \cite{Winslett90,Winslett95,Kat-Men91,Herzig96,BH93,Grahne91}
is similar to \kbr \  with the exception that $KB$ represents
dynamic world and $\alpha$ represents the effect of an action to
be performed. It is worth noting that under this interpretation
\kbu \ 
is nothing else but a very restricted form of reasoning about
action. The formal basis for \kbu \ has been proposed by Katsuno
and Mendelzon \cite{Kat-Men91} in the form of eight postulates,
referred  as the KM postulates.
The best-known solution to \kbu \ satisfying the KM postulates is
Winslett's PMA \cite{Winslett90}. 

A number of
researchers have observed \cite{BH93,Herzig96} that the KM postulates in the
context of classical formulation of \kbu \ can give rise to
unintuitive results. The example frequently given is this.
Suppose that \KB$=p$ and $\alpha=p\lor q$. Since \KB$\models
\alpha$, then by  postulate 2, we receive \KB$*\alpha=p$. This
result is clearly problematic. For instance, if $\alpha$ is the
effect of tossing a coin, where $p$ is {\em tails} and
$q$ is {\em heads}, we obviously do not want to conclude that
our world does not change after the action.

In recent years, a few \kbu \ formalisms trying to eliminate
unintuitive results have been proposed \cite{LUP97}. All of them
violate some of the KM postulates.

In this paper we propose   different intuitions standing behind   knowledge base update.
We assume that the knowledge about the world is generally incomplete and that this world can change dynamically as the result of
performing actions. 
 Roughly speaking, we consider the update formula $\alpha$
not as an effect of an action to be performed, but rather as an
observation about  world made by an agent.
If this observation  is consistent with the knowledge base, there is no reason to conclude  that an action has been performed.
Accordingly, in this case $\alpha$
is assumed to be just a new piece of information about the world.
Otherwise, we conclude  that a {\em single} action has been performed and
$\alpha$ is its, usually partial, effect. An example will help
to illustrate this.

Suppose I have a neighbour living in Warsaw.
Assume first that I have no information about where my neighbour is and where his car is. If I observe the neighbour's car
behind his house, I treat this observation  as a new piece of information increasing my knowledge about the world.
Assume now that   I know that 
yesterday my neighbour went by his car outside. 
Today, I observed that the car is parked behind his house.
The presence of the car clearly suggests that the action of
coming back to Warsaw has been performed by the neighbour. It is worth noting that 
the  observation, i.e. the presence of the car, is only a part of the
action's effect. Obviously, we should be able to infer more, namely
that the neighbour is in Warsaw  as well. Note that to make this
inference, we must know the full specification of all admissible
actions.


The paper is organized as follows. In section 2 we provide a general formalization 
of the problem and define our update operator referred to as {\it lazy knowledge base update operator} (\lkbu{}, for short). 
In section 3 we represent \lkbu{} in terms of Dijkstra's semantics. In section 4, we illustrate our update operator with a few
examples.
 Section 5 is devoted to formal properties of \lkbu{} operator. Finally, section 6
 contains concluding remarks.


\section{Formalization of the problem}

We are given a knowledge base \KB \  and an observation $\alpha$. 
If $\alpha$ is consistent with \KB,\  we treat it as new
information about the world, so the new \KB \  is just the old one
augmented with $\alpha$. Otherwise, we conclude that the world
has been changed as the result of performing an action. In this
case, our task is the following: (1)
 To identify the action that has been performed; (2)
 To describe the new knowledge base representing the world.


To resolve the above task, we have to know all admissible actions.
Suppose that these are \act.
Assume further that $\circ$ is an operator that, for a given \KB
\ 
and an action $A$, returns the new knowledge base
representing the world after executing the action\footnote{
The technical details concerning both the representation of
actions and the specification of $\circ$ will be presented later.}. 
Note that under these assumptions:
\begin{enumerate}


\vspace*{-1.5mm}
\item If  the performed action is $A_i$, the new
knowledge base \KB' \  is \KB$\circ A_i$.

\vspace*{-1.5mm}
\item Since $\alpha$ has been observed after executing the
action $A$ then \KB' should be restricted to (\KB$\circ A_i)\land \alpha$.

\vspace*{-2.5mm}
\item 
If we do not know which action has been performed, all we can
conclude is that the new knowledge base is 

\vspace*{-1.5mm}
\begin{equation}\label{og}
\bigvee_{i=1}^n ((\KB\circ A_i)\land \alpha).
\end{equation}

\vspace*{-2.5mm}
It is easy to see that the disjuncts of (\ref{og}) that are not equivalent
to false, specify all possible performed actions.
\end{enumerate}

In conclusion, our update operator, called lazy knowledge base
update and abbreviated to \lkbu \  is defined by 
\[
\KB *\alpha=\left\{\begin{array}{ll}
           \KB \land \alpha &amp; \mbox{\rm if \KB $ \land \alpha$  is satisfiable}\\
           \bigvee_{i=1}^n (( \KB \circ A_i)\land \alpha )&amp; \mbox{\rm
otherwise}
\end{array}\right.
\]










\section{\lkbu \  in terms of Dijkstra's semantics}\label{sec:4}
In this paper we assume that \KB \  and $\alpha$ are based on
classical propositional language, (with boolean constants $\top$ and $\bot$ standing for truth and falsity, respectively) and actions are represented 
 in terms of Dijkstra's semantics, originally developed to
reason about programs \cite{DijkstraScholten90}.


In \cite{DijkstraScholten90} we are provided with
a  very simple
programming language whose semantics is specified in terms of
formula transformers. More specifically,
with each command $S$ there are  associated three formula transformers,
called   the {\em weakest
precondition},  the {\em weakest liberal
precondition}  and the {\em strongest postcondition},  denoted
by  $wp$, $wlp$ and  $sp$, respectively. In this paper we ignore the first two transformers, because they will not be used in the sequel.
Before providing the meaning
of  the $sp$ transformer, two remarks are in order.
%\footnote{We ignore the {\em weakest liberal precondition} transformer, considered in \cite{DijkstraScholten90},
%because it will not be used in the sequel.}

Firstly, we assume here that the programming language under
consideration contains one type of variables only, namely Boolean
variables.
To be in accord with our earlier terminology,
 Boolean variables will be referred to as {\em atoms}.
Secondly,
in Programming Languages terminology, interpretations are usually referred
to as {\em states}. We shall use this latter term here because it seems to be
more appropriate  in dynamic settings.


If $\alpha$ is a formula, $x$ is a variable and $\beta$ is a
boolean expression, then 
$\alpha[x\leftarrow \beta]$ denotes a formula obtained from
$\alpha$ by replacing all free occurrences of $x$ by $\beta$.

Let $p$ be an atom and suppose that $\alpha$ is a formula.
By
$\exists p. \alpha$  we denote  the formula $\alpha[p\leftarrow \top]\lor
\alpha[p\leftarrow\bot]$. 

The $sp$ transformer
 is to be understood as follows.
For each command $S$ and each formula $\alpha$:
$sp(S,\alpha)$ is the formula whose  models are precisely all
 states such that each of them can be reached  by starting execution of  $S$ in
some state satisfying $\alpha$.


\subsection{ SDPL: A Simple Dijkstra Programming Language}

The considered programming  language  consists of {\em skip} command,
{ \em assignment} command,
 {\em sequential
composition} of commands and  {\em alternative}
 command. Semantics of these commands is specified in terms of $sp$ transformer as follows.
\begin{enumerate}
\item {\bf The {\em skip} command.}
This is the ``empty'' command. 

\vspace*{-1.5mm}
      \[
        sp(skip,\alpha)= \alpha.
       \]
\vspace*{-3mm}


\item {\bf
 The {\em  assignment} command.}
This command is of the form $x:=e$, where
$x$ is a (Boolean) variable  and
 $e$ is a (Boolean)  expression.

\vspace*{-1.5mm}
\[
sp(x:=e,\alpha)=\exists y.((x\equiv e[x\leftarrow y])\wedge\alpha[x\leftarrow y]),
\]

\vspace*{-1.5mm}
where $y$ is a fresh variable.
If the variable $x$ does not occur in the expression $e$, the above equation
 can be simplified to

\vspace*{-1.5mm}
\begin{equation}\label{simpl}
sp(x:=e, \alpha)= (x\equiv e) \wedge \exists x.
\alpha
\end{equation}

\item {\bf The {\em sequential composition} command.}
This command is of the form $S_1;S_2$, where $S_1$ and
$S_2$ are any commands. 


       \[
        \begin{array}{rcl}
 %         wp(S_1;S_2 ,\alpha )&amp;=&amp; wp(S_1, wp(S_2, \alpha)).\\
%   \hspace*{3mm}


         sp(S_1;S_2 ,\alpha )&amp;=&amp;sp(S_2, sp(S_1, \alpha)).
        \end{array}
        \]

\item {\bf The {\em alternative} command.}
This command is of the form
\begin{equation} \label{if}
 \begin{array}{lllllllll}
  \mbox{\bf if}&amp;B_1\limp S_1&amp;\pud &amp;B_2\limp
  S_2&amp;\pud&amp;\cdots
 &amp;\pud&amp;B_n\limp S_n &amp;
  \mbox{\bf fi}
 \end{array}
  \end{equation}
  where $B_1,\ldots, B_n$ are Boolean expressions and
  $S_1,\ldots, S_n$ are any commands. $B_1,\ldots, B_n$ are called
{\it guards} and expressions of the form $B_i\limp S_i$
are called {\it guarded commands}.
  In the sequel, we refer to
the general command (\ref{if}) as IF. The command is executed as
follows.
If none of the guards is true, then the execution is equivalent to
skip command. Otherwise,
one guarded command $B_i\limp S_i$ with true $B_i$ is
{\it randomly} selected  and $S_i$ is executed.\footnote{Note
that when more than one guard is true, the selection of a
guarded command is nondeterministic.}
 

\[
\begin{array}{rll}
%    wp({\rm IF},\alpha )&amp;=&amp;
%                  \bigwedge^{n}_{i=1}(B_i\implies
%                  wp(S_i,\alpha)) \land (\bigwedge^n_{i=1} \neg B_i)
%\implies \alpha \\ &amp;&amp;\\
   sp({\rm IF},\alpha )&amp;=&amp;
                  \bigvee^{n}_{i=1}(sp(S_i, B_i\wedge\alpha))
\lor (\bigwedge^n_{i=1}\neg B_i)\land \alpha.
\end{array}
\]

\end{enumerate}
In the sequel we shall use the following two properties of the $sp$ transformer:\\
For any command $S$ and any
formulae $\alpha$ and $\beta$ 
\begin{eqnarray}\label{sp}
&amp;&amp;sp(S,\bot)=\bot\\
\label{sp1}
&amp;&amp;sp(S, \alpha\vee \beta)\equiv sp(S,\alpha)\vee sp(S,\beta).
\end{eqnarray}


\subsection{Computing eliminants}

Recall that by $\exists p. \alpha$  we denote  the formula $\alpha[p\leftarrow \top]\lor
\alpha[p\leftarrow\bot]$. 
A formula of the form $\exists p. \alpha$
 is called an {\em eliminant of 
 $p$ in $\alpha$}.\footnote{Intuitively, such an eliminant can be viewed
as a formula  representing  the same knowledge as $\alpha$ 
about all atoms except $p$  and providing  no information about the
  atom  $p$.
The reader interested in a detailed theory of eliminants should consult
\cite{Brown90}.}
Computing eliminants is crucial in computing the $sp$ transformer.
In the literature (see \cite{Brown90}), eliminants are computed
by first transforming  $\alpha$  into its
disjunctive normal form. Since transforming a knowledge base
into its  disjunctive normal form is very expensive, we provide
a new algorithm to compute eliminants. This algorithm is based
on a
DLS algorithm, originally developed to reduce second-order
formulae into their first-order equivalents (see \cite{dls}).   
The DLS algorithm is based on Ackermann's lemma \cite{ack35}.
 
The algorithm consists of three phases.\\[2mm]
{\bf Phase 1.  Preprocessing}\\
The purpose of this phase is to transform the formula $\exists
p.A$ into the form 
\begin{equation}\label{wz}
\exists p. [(A_1(p)\land B_1(p))\lor \cdots\lor (A_n(p)\land B_n(p))]
\end{equation}
where $A_i(p)$ contains positive and $B_i$ negative ocurrences
of the atom $p$.
\begin{enumerate}
\item Eliminate $\impl$ and $\wtt$ and move $\neg$ to the right.
\item Distribute all top-level conjunctions over the
disjunctions containing both possitive and negative occurrences
of $p$. For this purpose, apply the  equivalences
 $A\land (B\lor C)\equiv (A\land B)\lor (A\land C)$ and
$(A\lor B)\land C\equiv (A\land C)\lor (B\land C)$
only if $B\lor C (A\lor B)$ have both positive and negative
occurrences of $p$ until the resulting formula is in the form (\ref{wz}).
\item Replace (\ref{wz}) by its equivalent given by
\begin{equation}\label{wz1}
\exists p. (A_1(p)\land B_1(p))\lor \cdots\lor \exists p.(A_n(p)\land B_n(p))
\end{equation}
\end{enumerate}
{\bf Phase 2. Preparation to Ackermann's lemma}\\
Repeat this step for each $1\leq i\leq n$
\begin{enumerate}
\item Transform $A_i(p)$ to the form
$(p\lor C_i)\land D_i$
or $B_i(p)$ to the form
$(\neg p\lor C_i)\land D_i$,
where $C_i,D_i$ do not contain $p$.
This transformation is always possible using thec equivalences
 $(A\land B)\lor C\equiv (A\lor C)\land (B\lor C)$ and
 $A\lor (B\land C)\equiv (A\lor B)\land (A\lor C)$.
\end{enumerate}
{\bf Phase 3.  Application of Ackermann's lemma}\\
Use Lemma 4.1 (Ackermann's Lemma) from \cite{dls}.\\
Repeat this step for each $1\leq i\leq n$
\begin{enumerate}
\item Replace 
 $\exists p (p\lor C_i)\land B'_i(p\leftarrow \neg p)$ by
$B'_i(p\leftarrow \alpha)$
or
$\exists p (\neg p\lor C_i)\land A'_i(p)$ by
$A'_i(p\leftarrow \alpha)$.  \koniec
\end{enumerate}





\section{Examples}
In this section we illustrate our update operator with a few  examples.
\begin{ex}\nl 
There are two fluents, $n$ and $c$, standing for
{\em my neighbour is in Warsaw} and {\em his car is in Warsaw},
respectively, and four actions: {\em leave(Warsaw)-by-car}, 
{\em leave(Warsaw)-by-train}, {\em
come-back(to Warsaw)-by-car} and {\em come-back(to Warsaw)-by
train}, specified as follows:
\begin{enumerate}

\vspace*{-1.5mm}
\item[$A_1:$] {\em leave-by-car}:
 {\bf if} $c\land n \limp c:=\bot; n:=\bot \pud \neg c\lor \neg n \limp
skip$ {\bf fi}

\vspace*{-1.5mm}
\item[$A_2:$] {\em leave-by-train}:
 {\bf if} $ n \limp  n:=\bot \pud  \neg n \limp
skip$ {\bf fi}

\vspace*{-1.5mm}
\item[$A_3:$] {\em come-back-by-car}:
 {\bf if} $\neg c\land \neg n \limp c:=\top; n:=\top \pud  c\lor  n \limp
skip$ {\bf fi}

\vspace*{-1.5mm}
\item[$A_4:$] {\em come-back-by-train}:
 {\bf if} $\neg n \limp  n:=\top \pud  n \limp
skip$ {\bf fi}.
\end{enumerate}
Assume first that \KB=$\neg n \land \neg c$ and our observation
$\alpha$ is $n$. Since \KB$\land \alpha$ is unsatisfiable,
\KB$*\alpha = \bigvee_{i=1}^4 sp(A_i,\KB)\land \alpha \equiv
[sp(A_3,\KB)\land \alpha]\lor
[sp(A_4,\KB)\land\alpha]$\footnote{Remaining disjuncts are reduced
to false.}$\equiv (c\land n)\lor (\neg c\land n)\equiv n$.

Note that it is impossible to determine how my heighbour came
back to Warsaw without an additional observation concerning his car.

Suppose now that \KB{} is as before but $\alpha$ is $c$. Again
\KB$\land \alpha$ is unsatisfiable, so 
\KB$*\alpha = \bigvee_{i=1}^4 sp(A_i,\KB)\land \alpha \equiv
sp(A_3,\KB)\land \alpha \equiv c \land n$.

Note that now we can conclude additional information, namely
that my neighbour is in Warsaw. \koniec
\end{ex}

The next example shows that it is sometimes possible to infer
new information that is not an effect of a performed action.
\begin{ex}\nl
There are two fluents $km$, standing for {\em my son knows
undergraduate maths}, and $pm$, standing for {\em my son passed
undergraduate maths exam}. Suppose that there is one action $se$
({\em my son stand to undergraduate maths exam}), defined as
\begin{enumerate}
\item[] {\bf if} $km \limp  pm:=\top \pud  \neg km \limp
pm:=\bot$ {\bf fi}.
\end{enumerate}
Assume further that \KB{} is $\neg pm$ and $\alpha$ is $pm$. Since
\KB$\land \alpha$ is unsatisfiable, we infer that the action
$se$ has
been performed and new \KB{} is $sp(se,\KB{})\land \alpha\equiv
(pm\land km \lor \neg pm\land \neg km)\equiv pm\land km$. \koniec
\end{ex}
\begin{ex}\nl
There are three fluents denoting a colour of the wall: {\it
blue}, {\it green}, {\it red}  and three actions: {\it
paint-blue}, {\it
paint-green}, {\it
paint-red} defined as:
\begin{enumerate}
\item[] {\it paint-blue: } $blue:=\top;green:=\bot;red:=\bot$
\item[] {\it
paint-green: } $blue:=\bot;green:=\top;red:=\bot$
\item[] {\it paint-red: } $blue:=\bot;green:=\bot;red:=\top$
\end{enumerate}
Assume first that \KB$=blue\land \neg green\land \neg red$ and
$\alpha=blue\lor green$. Since \KB$\land \alpha$ is satisfiable,
\KB$*\alpha=\KB \land \alpha \equiv \KB$.

It is worth noting that the disjunctive formula $\alpha$ is not
treated here as an effect of a non-deterministic action but
rather as an uncertain observation (possibly due to noisy sensors).

Assume now that \KB{} is as before and $\alpha$ is $green \lor red$.
Since \KB$\land \alpha$ is unsatisfiable, we conclude that an
action has been performed.
\begin{eqnarray*}
\KB*\alpha&amp;=&amp;sp(\mbox{\it paint-blue},\KB)\land (green \lor red) \\
&amp;\lor&amp;
sp(\mbox{\it paint-green},\KB)\land (green \lor
red)\\ 
&amp;\lor&amp; sp(\mbox{\it paint-red},\KB)\land (green \lor red)\\
&amp;\equiv&amp; \neg blue
\land (green \land \neg red \lor \neg green \land red).\;\; \koniec
\end{eqnarray*}
\end{ex}



\section{Formal properties of the \lkbu{} operator}

As we remarked earlier,
Katsuno \&amp; Mendelzon \cite{Kat-Men91} proposed a 
number of postulates (the KM postulates) that
they claim every update operator should satisfy.
In this section, we check these postulates with respect 
to \lkbu{}  operator.

Below, $KB$ is a knowledge base,  $\alpha$  is an update formula and
\act{} is the set of all admissible actions. 
We assume that this set is {\em complete} in the following 
sense: if \KB$\land \alpha$ is unsatisfiable for satisfiable \KB, 
then there exists at least one action $A_i$ such that $sp(A_i,\KB)\land \alpha$
is satisfiable. This intuitively means that each observation 
that is inconsistent with the current world can be explained by at 
least one action.
The KM postulates are the following:
\begin{enumerate}

\vspace*{-1.5mm}
\item[(U1)] $KB\star \alpha$ implies $\alpha$.

\vspace*{-1.5mm}
\item[(U2)] If $KB$ implies $\alpha$, then $KB\star \alpha$
 is equivalent to $KB$.

\vspace*{-1.5mm}
\item[(U3)] If both $KB$ and $\alpha$ are satisfiable, then $KB\star\alpha $ is
also satisfiable.

\vspace*{-1.5mm}
\item[(U4)] If $KB_1\equiv KB_2$ and $\alpha_1\equiv \alpha_2$, then
$KB_1\star \alpha_1\equiv KB_2\star \alpha_2$.

\vspace*{-1.5mm}
\item[(U5)] $(KB\star \alpha_1)\land \alpha_2$ implies $KB\star
 (\alpha_1\land \alpha_2)$.

\vspace*{-1.5mm}
\item[(U6)] If $KB\star \alpha_1$ implies $\alpha_2$ and
$KB\star \alpha_2$ implies $\alpha_1$, then $KB\star \alpha_1
\equiv KB\star \alpha_2$.

\vspace*{-1.5mm}
\item[(U7)] If $KB$ is complete, i.e.\ has at most one model,
then $(KB\star \alpha_1)\land (KB\star \alpha_2)$ implies
$KB\star (\alpha_1\lor \alpha_2)$.

\vspace*{-1.5mm}
\item[(U8)] $(KB_1\lor KB_2)\star \alpha \equiv (KB_1\star \alpha)\lor
(KB_2\star \alpha).$
\end{enumerate}


\begin{tw} \nl The \lkbu{}  operator satisfies the postulates (U1) -- (U7).\\
{\bf Proof:} We start with the following
\begin{lemma}\label{lem}\nl If $\KB$ is unsatisfiable, then 
$\KB *\alpha$ is equivalent to $\bot$, for any $\alpha$.\\
{Proof} of the lemma: Follows immediately from (\ref{sp}). \koniec
\end{lemma}
In view of Lemma \ref{lem}, it is obvious that the postulates
(U1) -- (U7) hold if \KB{} is unsatisfiable. We can, therefore, assume
that \KB{} is satisfiable. 
\begin{enumerate}
\item[(U1)] and (U4) are straightforward.

\vspace*{-1.5mm}
\item[(U2)] Since \KB{} implies $\alpha$, \KB{}  
and \KB$\land \alpha$ are equivalent,
and thus, since \KB{} is satisfiable,  \KB$\land \alpha$ is satisfiable. 
In conclusion, \KB$*\alpha$ is \KB$\land \alpha$, and so, 
\KB$*\alpha$ is equivalent to \KB.

\vspace*{-1.5mm}
\item[(U3)] If \KB$\land \alpha$ is satisfiable, 
the postulate obviously holds. Assume therefore, that \KB$\land \alpha$ is
unsatisfiable. Then \KB$*\alpha = \bigvee_{i=1}^n sp(A_i,\KB)\land \alpha$,
and so, \KB$*\alpha_1$ is satisfiable by the assumption that the 
set \act{} is complete.
%\item[(U4)] Straightforward.

\vspace*{-1.5mm}
\item[(U5)] If
 $\KB\land \alpha_1$ is satisfiable, the postulate clearly holds.
Assume, therefore, that \KB$\land \alpha_1$ is unsatisfiable. 
Then \KB$*\alpha_1 = \bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_1$, 
and so, (\KB$*\alpha_1)\land \alpha_2=[ \bigvee_{i=1}^n sp(A_i,\KB)\land 
\alpha_1]\land \alpha_2=\bigvee_{i=1}^n[ sp(A_i,\KB)\land \alpha_1\land 
\alpha_2]$. On the other hand, since \KB$\land\alpha_1$ is 
unsatisfiable, \KB$\land\alpha_1\land\alpha_2$ is also unsatisfiable, 
and hence, \KB$*(\alpha_1\land\alpha_2)=\bigvee_{i=1}^n[ sp(A_i,\KB)\land 
\alpha_1\land \alpha_2]$.

\vspace*{-1.5mm}
\item[(U6)] Assume first that $\KB\wedge\alpha_1$ is satisfiable.
Then, $\KB *\alpha_1$ is $\KB\wedge\alpha_1$. Hence, since
$\KB*\alpha_1$ implies $\alpha_2$, $\KB\wedge\alpha_2$ is also
satisfiable, and so,  $\KB*\alpha_2$ is $\KB\wedge\alpha_2$.
Thus, we know that $\KB\wedge\alpha_1$ implies $\alpha_2$ and
$\KB\wedge\alpha_2$ implies $\alpha_1$, what immediately implies
that $\KB\wedge\alpha_1$ and $\KB\wedge\alpha_2$, and so
$\KB *\alpha_1$ and $\KB *\alpha_2$, are equivalent.
Assume now that $\KB\wedge\alpha_1$ is unsatisfiable. Then, by a
similar argument as before, we conclude that
$\KB\wedge\alpha_2$ is also unsatisfiable.   
Thus, we infer that $\bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_1$
implies $\alpha_2$ and $\bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_2$
implies $\alpha_1$. Hence, by propositional logic alone,
we conclude that $\bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_1$
and $\bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_2$, and so,
$\KB *\alpha_1$ and $\KB * \alpha_2$, are equivalent.

\vspace*{-1.5mm}
\item[(U7)] If at least one of $\KB\wedge\alpha_1$,
$\KB\wedge\alpha_2$ is satisfiable, the postulate clearly holds.
(Note that in this case $\KB\wedge(\alpha_1\vee\alpha_2)$
is also satisfiable.)
Assume, therefore, that $\KB\wedge\alpha_1$ and
$\KB\wedge\alpha_2$ are both unsatisfiable, what implies that
$\KB\wedge(\alpha_1\vee\alpha_2)$ is also unsatisfiable.
Then $\KB*\alpha_1 \wedge \KB* \alpha_2$ is equivalent to
(*) $\bigvee_{i=1}^n sp(A_i,\KB)\land \alpha_1\wedge\alpha_2$
and $\KB *(\alpha_1\vee\alpha_2)$ is equivalent to
(**) $\bigvee_{i=1}^n sp(A_i,\KB)\land (\alpha_1\vee\alpha_2)$.
Obviously, (*) implies (**). Note that we did  not use the
assumption that $KB$ is complete. \koniec
\end{enumerate}
\end{tw}
It should be stressed that postulate (U8) need not to hold for the 
\lkbu{} operator. To see this, assume that $KB_1$ is
$\neg p\wedge q$, $KB_2$ is $p\wedge\neg q$ and $\alpha$ is
$p$. Suppose further that there is one action, $A$, given by
$p$:=$\top$. Then $(KB_1\vee KB_2)*\alpha$ is equivalent to
(*) $p\wedge\neg q$, whereas $(KB_1 *\alpha)\vee (KB_2*\alpha)$
is equivalent to (**) $p$. Obviously, (*) and (**) are not equivalent.


The \lkbu{} operator behaves similarly like belief revision operator
of \cite{agm85} if $\alpha$ is consistent with \KB{}.
Accordingly, one may suspect that  the \lkbu{} operator
satisfies some of the  AGM postulates that do not hold for the classical
update operator. The next theorem, whose proof is straightforward, shows that this is indeed the case.
\begin{tw} 
\nl The \lkbu{} operator satisfies the following postulates:
\begin{enumerate}
\item[(U9)] If $KB\wedge\alpha$ is satisfiable, then $KB*\alpha
\equiv KB\wedge\alpha$.
\item[(U10)] If $(KB *\alpha_1)\wedge\alpha_2$ is satisfiable, then
$KB*(\alpha_1\wedge\alpha_2)$ implies $(KB *\alpha_1)\wedge
\alpha_2$.
\end{enumerate}

\end{tw}

\section{Conclusions}

In this paper, we have proposed a new approach to knowledge base
update, called \lkbu. The main difference between \lkbu{} and
other formalisms directed at knowledge base update is that an
update formula, if consistent with a knowledge base, is regarded
not as an effect of an action but rather as a piece of new
information about the considered world.

We have formalized \lkbu{} using Dijkstra's semantics,
originally developed to reason about programs. Also, we have
examined formal properties of our formalism with respect to
update postulates of Katsuno and Mendelzon.

In this paper we do not consider integrity constraints. However
this extension can be easily incorporated by using a technique
proposed in \cite{m97}.

As we observed (Examples 1, 3), in general, an update formula
$\alpha$ do not allow to extract a single performed action.
Instead, we receive a number of actions corresponding to
$\alpha$. An interesting topic to consider is to specify a
minimal set of additional observations which could eliminate
some of these actions. For instance, in Example 1 (first part)
the new observation that the car is in Warsaw would eliminate
the action {\em come-back-by-train}. We plan to work on this
problem in the future.




\begin{thebibliography}{99}

\bibitem{ack35} W. Ackermann. Uutersuchungen 
 \"{u}ber das Eliminantionsproblem der mathematischen Logik.
 {\em Mathematische Annalen}, 110, 390-413, 1935.
 

\vspace*{-1.5mm} 
\bibitem{agm85} C. E. Alchourr\'{o}n, P. G\"{a}rdenfors,
D. Makinson. On the Logic of Theory Change: Partial Meet
Contraction and Revision Functions. {\em Journal of Symbolic Logic},
50, 1985, 510-530.
\bibitem{BH93} G. Brewka, J. Hertzberg. How to Do Things with Worlds:
on Formalizing Actions and Plans. {\em Journal of Logic and Computation}.
Vol. 3, No. 5, 1993, 517-532.

\bibitem{Brown90} F. M. Brown. {\em Boolean Reasoning}. Kluwer
Academic Publishers, 1990.

\bibitem{CorS:92}
M-O.~Cordier, P. Siegel.
\newblock A Temporal Revision Model for Reasoning about World Change.
\newblock In {\em Int'l. Conference on Principles of 
Knowledge Representation and Reasoning}, 
732-739, Morgan Kaufmann, 1992.









\bibitem{DijkstraScholten90} E. W. Dijkstra, C. S. Scholten.
{\em Predicate Calculus and Program Semantics}. Springer-Verlag, 1990.


\bibitem{LUP97} P. Doherty, W. {\L}ukaszewicz, E. Madali\'{n}ska-Bugaj.
\newblock The PMA and Relativizing Minimal Change for Action Update.
%In: {\em Proc. of the 6th Int'l Conference  on Principles of
%Knowledge Representation and Reasoning}. Morgan Kaufmann, 1998, 258-269.
{\em Fundamenta Informaticae} {\bf 44} (2000) 95-131.

\bibitem{dls} P. Doherty, W. \L{}ukaszewicz, A. Sza\l{}as. 
Computing Circumscription Revisited: A Reduction Algorithm. {\em Journal
of Automatic Reasoning}, {\bf 18}, 1997, 297-336.

%\bibitem{ism99} P. Doherty, W. \L{}ukaszewicz, E.  Madali\'{n}ska-Bugaj, E.
%Computing MPMA Updates Using Dijkstra's Semantics.
%{\em Proceedings of the 11th International Symposium, ISMIS'99}.
%Lecture Notes in Artificial Intelligence, {\bf 1609}, 1999, 271-281.
 



\bibitem{Herzig96} A. Herzig. The PMA Revisited. In: {\em Proc. of
the 5th Int'l. Conference on Principles of Knowledge Representation and
Reasoning}, Morgan Kaufmann,
1996, 40-50.


\bibitem{Grahne91} G. Grahne. Updates and Counterfactuals. In
{\em Proc. of the 2nd Int'l. Conference on Principles of
 Knowledge Representation and
Reasoning}, Morgan Kaufmann,
1991, 269-276.


\bibitem{Kat-Men91} H. Katsuno, A. O. Mendelzon. On the Difference between
Updating a knowledge base and revising it. In:  {\em Proc. of
the 2nd Int'l. Conference on Principles of Knowledge Representation and
Reasoning}, KR'91, Morgan Kaufmann,
1991, 387-395.


\bibitem{m97} Madali\'{n}ska-Bugaj, E. (1997) How to Solve Qualification
and Ramification Using Dijkstra's Semantics for Programming
Languages, in: {\it AI*IA-97: Advances in Artificial
Intelligence, Proceedings of 5th Congress of the Italian
Association for Artificial
Intelligence}, Springer-Verlag,  Lecture Notes in Artificial
Intelligence, {\bf 1321}, 381-392, 1997.


\bibitem{Nebel89} B. Nebel. A Knowledge Level Analysis of Belief
Revision. In: {\em Proceedings  of
the 5th International  Conference on Principles of Knowledge Representation and
Reasoning}, 
1989, 301-311.


%\bibitem{ValS:93}
%A.~del Val, Y.~Shoham.
%\newblock Deriving Properties of Belief Update from Theories of Actions (II).
%\newblock In {\em Proc. of the 13th Int'l.
%  Joint Conference on Artificial Intelligence}, pages 732--737,
%  1993.




\bibitem{Winslett90} M. Winslett. {\em Updating Logical Databases}.
Cambridge Tracks in Theoretical Computer Science. Cambridge University
Press, 1990.

\bibitem{Winslett95} M. Winslett. Updating Logical Databases.
In: D. Gabbay, A. Galton, J. A. Robinson (eds.). {\em Handbook of Logic in
Artificial Intelligence and Logic Programming}. Vol. 4 (Epistemic and
Temporal Reasoning), 1995, Oxford University Press, 133-174.

\end{thebibliography}


\end{document}

</pre></body></html>