\documentstyle[a4wide,tree-dvips,macros,examples]{article}
\setlength{\parskip}{0.1in}
\setlength{\parindent}{0in}
\setlength{\itemsep}{0in}


% AVM macros
%
% Use these with \tiny to get sensible looking FSs
% \tiny doesn't affect the internal text because this is explicitly set
% to \small below

\newcommand{\avmplus}[1]{{\setlength{\arraycolsep}{0.8mm}       
                       \renewcommand{\arraystretch}{1.1} %1.2
                       \left[                   
                       \begin{array}{l}
                       \\[-2mm] #1 \\[-2mm] \\ %2
                       \end{array}              
                       \right]
                    }}
%
\newcommand{\att}[1]{{\mbox{\small {\bf #1}}}}
\newcommand{\attval}[2]{{\mbox{\small #1}\ :\ {{#2}}}}
\newcommand{\attvaltyp}[2]{{\mbox{\small #1}\ :\ {\myvaluebold{#2}}}}
\newcommand{\myvaluebold}[1]{{\mbox{\small {\bf #1}}}}
\newcommand{\ind}[1]{{\setlength{\fboxsep}{0.5mm} \: \fbox{{\tiny #1}} \:}}
%
\def\implies{\rightarrow}
\hyphenation{dis-ambig-uate dis-ambig-uated dis-ambig-uation}

\newcommand {\lsembrac}         {\mbox{[ \kern -0.5 em [}}
\newcommand {\rsembrac}         {\mbox{] \kern -0.5 em ]}}
\newcommand {\sem} [1]          {{\lsembrac #1 \rsembrac}}
\newcommand {\etal} {{\it et al.}}
%\newcommand{\hidden}[1]{}
\newcommand{\hidden}[1]{#1}
% \csmodels is the consequence relation in a formula; \csmodel is the
% consequence relation in running text.
\newcommand {\csmodels}         {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5
em $\approx$}\hspace*{0.5em}}
\newcommand {\csmodel}  {\mbox{$\mid$ \kern -0.5 em $\approx$}}

\newcommand {\notcsmodels} {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em
$\approx$ \kern -1 em $/$}\hspace*{0.5em}}

\newcommand {\csproves}         {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em $\sim$}\hspace*{0.5em}}
\newcommand {\csprove}  {\mbox{$\mid$ \kern -0.5 em $\sim$}}

\newcommand {\notcsproves} {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em $\sim$ \kern -1 em $/$}\hspace*{0.5em}}

\newcommand{\pdumodel}{\csmodel_{pdu}}
\newcommand{\pduprove}{\csprove_{pdu}}

\newcommand{\yadumodel}{\csmodel_{yadu}}
\newcommand{\yaduprove}{\csprove_{yadu}}

\newcommand{\cunifymodel}{\models_{\cunify}}
\newcommand{\cunifyprove}{\vdash_{\cunify}}

\newcommand{\unifymodel}{\models_{\unify}}
\newcommand{\unifyprove}{\vdash_{\unify}}

\newcommand{\cddunifymodel}{\models_{\cddunify}}
\newcommand{\cddunifyprove}{\vdash_{\cddunify}}

\newcommand{\csddunifymodel}{\models_{\mbox{\tiny $\csddunify$}}}
\newcommand{\csddunifyprove}{\vdash_{\mbox{\tiny $\csddunify$}}}



\newcommand{\tag}[1]{\mbox{\^{ #1 }}}

\newcommand{\happyface} {\mbox{\Large
$\bigcirc$\small\raisebox{-0.02in}{\hspace*{-0.17in}$\smile$}
\raisebox{0.06in}{\hspace*{-0.17in}.\hspace*{0.03in}.}}\normalsize
\hspace{0.05in}}
% Used as in, e.g., \sem{\phi}^{\rm DPL}_{M,w,t}
%
% Unification
% -----------
\newcommand{\subsumes}{\op{\sqsubseteq}}
\newcommand{\subsumedby}{\sqsupseteq}
\newcommand{\subsumeseq}{\op{\sqsubseteq}}
\newcommand{\generalize}{\sqcup}
\newcommand{\unify}{\sqcap}
\newcommand{\sunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}_{s}}
\newcommand{\cunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}_{c}}
\newcommand{\dunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}}
\newcommand{\ddunify}{\stackrel{{\scriptscriptstyle <>}}
                              {\sqcap}}
\newcommand{\cddunify}{\stackrel{{\scriptscriptstyle <}} 
                              {\sqcap}_{ca}}
% changed from <> because it's asymmetric 
\newcommand{\csddunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}_{cs}}
% changed from <> because it's asymmetric
\newcommand{\unifyset}[1]{\bigsqcap #1}
\newcommand{\join}{\sqcap}
\newcommand{\meet}{\sqcup}
\newcommand{\setlist}[1]{\{ #1 \}}
\newcommand{\setstack}[1]{ \left\{ 
                           \begin{array}{l} #1 \end{array} \right\} }
\newcommand{\setcomp}[2]{\setlist{#1 \, \mid \, #2 }}
%

\newcommand{\modal}[1]{\langle #1 \rangle}



\newtheorem{defn}{Definition}
\newtheorem{translation}{Translation}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}


\begin{document}

\title{Order Independent Typed
Default Unification}

\author{{\bf Alex Lascarides}\\
{\small Centre for Cognitive Science {\em and}}\\ {\small Human
Communication Research Centre,}\\ {\small University of Edinburgh,}\\
{\small 2, Buccleuch Place,}\\ {\small Edinburgh, EH8 9LW,}\\ {\small
Scotland, UK}\\ {\small {\tt alex@cogsci.ed.ac.uk}}
\and
{\bf Ann Copestake}\\ {\small Computer Laboratory, University of
  Cambridge, {\em and}}\\ {\small Center for the Study 
of Language and Information,} \\ {\small Stanford University,}\\
{\small Cordura
Hall,}\\ {\small Stanford, CA 94305,}\\ {\small USA}\\ {\small {\tt
aac@csli.stanford.edu}}}

\maketitle
 
\begin{abstract}
We describe an order independent typed default unification function,
which allows default reentrancies and values on more general types to
be overridden by conflicting default information on more specific
types.  This therefore extends the order independent default
unification operations in Young and Rounds (1993) and Lascarides {\em
et al.} (in press), thereby increasing the range of linguistic
generalisations that can be expressed.
\end{abstract}



\section{Introduction}
\label{intro}

Many computational linguists have argued that default inheritance is
useful for encoding linguistic generalisations which have exceptions
(Dealemans {\em et al}, 1992).  But although there have been several
approaches to formalising default inheritance within feature structure
languages by defining an operation of default unification (e.g. Bouma
1992, Russell {\em et al} 1991, Copestake 1993), these have failed to
achieve the combination of perspicuity, declarativity and
expressibility familiar from unification-based approaches to
non-default inheritance.  We believe the following properties are
necessary for default unification to have these qualities:
\begin{enumerate}
\item Non-default information can be distinguished from
default information and is always preserved.
\item Default unification behaves like monotonic unification in the
cases where monotonic unification would succeed.
\item Default unification returns a single result, deterministically.
\item Defaults can be given a precedence ordering such that more
specific information overrides less specific information.
\item Default unification can be described using a binary, order
independent (i.e., commutative and associative) operation.
\item Default unification never fails unless there is conflict in
non-default information.
\end{enumerate}

Most definitions of default unification have been based on Kaplan's
sketch of priority union (Kaplan, 1987) and are asymmetric since one
feature structure ({\sc fs}) is taken to be indefeasible while the
other is defeasible.  This operation isn't commutative or associative
(Carpenter, 1993).  Although there are some
applications for which an asymmetric operation is useful, the
order-dependency makes it undesirable as a basis for inheritance.
Furthermore, since these definitions don't meet our criterion~4, the
inheritance hierarchy has to be defined separately.  The most common
linguistic application for
default inheritance is  to encode lexical
generalisations (Boguraev and Pustejovsky, 1990;
Briscoe \etal, 1990; Vossen and Copestake, 1993; Daelemans 1987; Evans
and Gazdar 1989a,b; Flickinger \etal, 1985; Flickinger, 1987;
Flickinger and Nerbonne, 1992; Krieger and Nerbonne, 1993; Shieber,
1986 and others).  Having an ordering dependent operation in the
lexicon itself is not a serious problem, because all the entries to be
unified are in a fixed hierarchy and an inheritance order can indeed be
imposed.  
But in a discourse situation, one cannot predict which
pieces of information are to be unified {\em in advance} of starting
the discourse parsing process.  So the interface between discourse
processing and order dependent lexical processing would have to take
into account the order in which the unification operations are done,
which is impractical (see Lascarides and Copestake 1995 for further
discussion).

Young and Rounds define an order independent version of default
unification (Young and Rounds, 1993).  But it doesn't meet
criterion~4.  They use Reiter's default logic (Reiter, 1980) to model
the operation.  So the most straightforward way of extending the
definition to meet criterion~4 would be to extend Reiter's default
logic so that it validates specificity.  But
 as Asher and Morreau (1991), Lascarides and Asher
(1993) and Lascarides {\em et al} (in press) argue, all such extensions to
Reiter's default logic either impose ordering constraints on the
application of logical axioms in proofs (e.g., Konolige, 1988), or
they impose a context-sensitive translation of the premises into the
formal language (e.g,. Brewka, 1991).  So extending Young and Rounds'
definition in this way comes at the cost of an underlying formal
semantics which has separately defined order constraints on the
logical axioms, or context sensitive translation.

Lascarides {\em et al} (in
press) use conditional logic to extend Young and Rounds' definition to
one on typed feature structures, called Persistent Default Unification
({\sc pdu}).  
They use conditional logic precisely because these logics are able to
validate nonmonotonic patterns of inference involving specificity
without imposing ordering constraints on the application of axioms or
imposing context sensitive translation on the premises.
In order to allow default inheritance in type
hierarchies, precedence of default values in {\sc pdu} is determined
by the specificity of the types at which the default is introduced.
{\sc pdu} thus meets criterion 4 for non-reentrant information.  But it
fails to validate the overriding of default reentrancy by conflicting
default values introduced by a more specific type.  In this situation,
the default reentrancy survives and the default value on the shared
node is $\bot$, indicating unification failure.  

This failure to fully
meet criterion 4 restricts {\sc pdu}'s linguistic application and also
causes problems in interpreting {\sc fs}s containing $\bot$.
For example, consider a representation of the morphology of English
verbs where there is an attribute for the past tense form and another
for the past particle.  Normally these are the same, and this can be
represented by default reentrancy.  The forms differ in some classes
of irregular verbs (e.g. {\it speak, spoke, spoken}), but the
specification of the vowel change and suffixation for this class ought
itself to be defeasible, because of a subclass
of these verbs, such as {\it weave}, which
are also found with the regular suffixation pattern ({\it wove}/{\it
weaved}, {\it woven}/{\it weaved}).  

In this paper, we define an order independent typed default
unification operation ($\ddunify$) called {\sc yadu} (Yet Another
Default Unification), which allows default reentrancies to be
overridden by default values introduced by a more specific type and
thus provides the first definition of default unification that fulfills
all of the above criteria.  


\section{Typed Default Feature Structures}

We wish to define an order independent default unification operation
on typed information.  Copestake (1993) and Grover {\em et al} (1994)
define default unification operations that operate over typed feature
structures ({\sc tfs}s).  In both cases, the operation is asymmetric,
however.  The {\sc tfs} on the left hand side of the operation is
treated as indefeasible, and the one on the right hand side is treated
as defeasible.  Roughly speaking, the result of unifying these two
{\sc tfs}s together is the indefeasible {\sc tfs} unified with as much
information as possible from the defeasible {\sc tfs} while remaining
consistent.  An example is shown in Figure~\ref{priorityunioneg}.
\begin{figure}
\begin{center}
\begin{tabular}{lll}
{\tiny $\left(
\avmplus{\attvaltyp{F}{c}\\
                 \attvaltyp{G}{c}}

\mbox{\normalsize $\dunify$} 

\avmplus{\attvaltyp{F}{a}\\
                 \attvaltyp{G}{b}}
\right)

\mbox{\normalsize $\dunify$} 

\avmplus{\attval{F}{\ind{1}}\\
                 \attval{G}{\ind{1}}}$ } & $=$ & {\tiny
$\avmplus{\attval{F}{\ind{1} \myvaluebold{c}}\\
\attval{G}{\ind{1}}}$}\\[0.1in]
% next line
{\tiny $\avmplus{\attvaltyp{F}{c}\\ \attvaltyp{G}{c}}$}

$\dunify$

{\tiny $\left(
\avmplus{\attvaltyp{F}{a}\\
                 \attvaltyp{G}{b}}

\mbox{\normalsize $\dunify$}

\avmplus{\attval{F}{\ind{1}}\\
                 \attval{G}{\ind{1}}}
\right)$
} & $=$ & {\tiny $\avmplus{\attvaltyp{F}{c}\\ \attvaltyp{G}{c}}$}
\end{tabular}
\end{center}
\caption{Non-associativity of Asymmetric Default Unification}
\label{priorityunioneg}
\end{figure}
Clearly, an asymmetric default unification is non-commmutative,
because by changing the order of the arguments, one changes which
information is default and which is non-default.  The examples in
Figure~\ref{priorityunioneg} also show that such an operation is
non-associative.

Our demand for order independence requires us to define a symmetric
operation.  But this means that we cannot treat one {\sc tfs} as
specifying wholly indefeasible information and the other as wholly
defeasible, as one does in Figure~\ref{priorityunioneg}.  Rather, one
must explicitly mark in the information structures which information
is to be treated as default and which is non-default.  The standard
language of {\sc tfs}s doesn't make such distinctions.  But Young and
Rounds (1993) and Lascarides {\em et al.} (in press) demonstrate that
it's a necessary prerequisite for defining a symmetric default
binary operation.
Consequently, we must extend the
representation of
typed feature structures so that they have the
properties essential for successfully defining a default unification
operation that meets the criteria we specified in section \ref{intro}.
First, these structures must keep
default and non-default information distinct.  Second, they must
keep track of certain default information that was overridden during
unification, and so doesn't appear in the feature structure itself.
This is because this information must
sometimes influence the results of subsequent default unifications
if it is to meet the specified criteria.
The purpose of this section is to extend the representation of typed
information to go beyond {\sc tfs}s in the required
 manner.  We do it in a similar way to that
deployed in Lascarides {\em et al} (in press).  We will then define
the default unification operation over these extended representations.

We refer to these more refined information structures as typed default
feature structures or {\sc tdfs}s.  And we use the same notation as
Lascarides {\em et al} (in press) for representing them.  Informally,
a {\sc tdfs} contains a `double' typed feature structure ({\sc tfs})
in which the left hand {\sc fs} specifies what is indefeasible and the
right-hand {\sc fs} what is defeasible.  For instance in
(\ref{tdfs}), the value of the path {\sc f}$\cdot${\sc g} is {\bf b}
by default, but the existence of the paths {\sc f}$\cdot${\sc g} and
{\sc h}, and the value {\bf a} for {\sc h} are non-default.
\begin{examples}
\item   \label{tdfs}
{\tiny $\avmplus{\att{t}\\
\attval{F}{\avmplus{\attval{G}{\top}}}\\ \attvaltyp{H}{a}}$} $\left/
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{b}}}\\ \attvaltyp{H}{a}}$}
\end{array}
\right.
\left/
\begin{array}{l}
\{\langle
\mbox{\tiny $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$}
\mbox{{\bf t}}\rangle\}
\end{array}
\right.
$
\end{examples}

The third element in the structure is a {\it tail}.  {\em Tails}
record certain information from the unification history from which the
{\sc tdfs} was constructed.  A tail consists of a set of pairs, where
the first member of the pair is an atomic {\sc fs} (that is, a single
path or path equivalence) and the second member is a type.  These
pairs record default information that appeared in a {\sc tdfs} that
was used to build the {\sc tdfs} being considered, together with the
root type of that {\sc tdfs}.  Indeed the default information must be
{\em strictly} default, in the sense that it was strictly more
specific than the non-default information in that {\sc tdfs} (so it
was information that is not known for sure).  The position of this
root type in the type hierarchy, which we assume to be a finite
bounded complete partial order (Carpenter, 1992), determines the {\em
specificity} of the default information.  So during a series of default
unifications, tails will record default information from original {\sc
tdfs}s together with its specificity.  For example, suppose a {\sc
tdfs} has a tail of the following form:
\[
\begin{array}{r l}
\{ & \langle
\mbox{\tiny $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$}, \mbox{{\bf
t}}_1\rangle, \\ & \langle \mbox{\tiny
$\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}_2\rangle,\\ & \langle
\mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$},
\mbox{{\bf t}}_3\rangle\}
\end{array}
\]

This means that to produce the {\sc tdfs} with this tail, we unified:
a {\sc tdfs} that had a root type {\bf t}$_1$ and the strictly defeasible
path F:G:{\bf b}; a {\sc tdfs} that had root type {\bf t}$_2$ and
strictly defeasible path F:{\bf a}; and a {\sc tdfs} that had root
type {\bf t}$_3$ and strictly defeasible information that the F- and
G-paths share the same value.  These {\sc tdfs}s may have contained
further information; e.g., the latter {\sc tdfs} may have contained
the information that not only did F- and G- by default share the same
values, whatever they are, but also that indefeasibly, F's value is
{\bf c} and G's value is {\bf c}, as given in the {\sc tdfs} below
(ignoring the tail of this {\sc tdfs} for now):
\begin{examples}
\item   
{\tiny $
\avmplus{\att{t\mbox{$_3$}}\\
\attvaltyp{F}{c}\\
\attvaltyp{G}{c}}
\left/
\begin{array}{c}
\avmplus{\att{t\mbox{$_3$}}\\
\attval{F}{\ind{1}}\\
\attval{G}{\ind{1}}}
\end{array}
\right.
$ }
\end{examples}
The point is that tails don't record {\em all} the information that
forms part of the unification history; it only records the
strictly default information.  We explain this in more detail below.

We keep track of this information in the tail, because it is the cost
we must pay for being able to define default unification as a binary
order independent operation.  The assumption of a binary operation is
problematic since by the very definition of nonmonotonicity, one
cannot in general divide the premises into groups, work out the
inferences from those groups, and expect the inferences to survive the
whole.  The only way to gain order independence, therefore, is to
ensure that each time the binary operation is performed, it is
influenced by the necessary pieces of information that are `outside'
the immediate context of the {\sc fs}s it is unifying.  Tails cover
this necessary information by recording sufficient information for us
to define the default unification operation so that it has all the
desired properties.  In Lascarides {\em et al} (in press), we argued
in formal detail why tails were necessary.  The discussion is quite
lengthy and technical, and since it detracts from the main purpose of
this paper, which is to produce a more powerful default unification
than was presented there, we refer the reader to that paper for the
relevant formal motivation.

Indeed, the tails we have defined here contain more information than
those in Lascarides {\em et al.} (in press): specifically tails
here record default reentrancies.
This `bigger' tail
is the cost of defining a more powerful operation than {\sc pdu}; one
in which default reentrancies can be overidden by default values.

All {\sc tdfs}s will have tails, even ones that are not
derived from {\sc tdfs}s in the initial specification, but rather are
part of the initial specification itself.  We show how to define tails
for the initial specification shortly.  And we will refer to the
initial specifications of defaults as the {\em basic} {\sc tdfs}s, and
others as {\em derived} {\sc tdfs}s.

We can make some abbreviations, so that the `double' {\sc avm}
notation can be factored across individual paths into a single {\sc
avm} representation where we have $\mbox{{\em IndefeasibleValue}} /
\mbox{{\em DefeasibleValue}}$
which can be abbreviated to $\mbox{{\em IndefeasibleValue}}$ where
$\mbox{{\em IndefeasibleValue}}$ is the same as {\em DefeasibleValue},
and $/\mbox{{\em DefeasibleValue}}$ for $\top/\mbox{{\em
DefeasibleValue}}$, without ambiguity ($\top$ is the most general
type).  We can also omit the tail when it can be determined from the
default {\sc fs}.  That is, we omit the tail when it records exactly
the strict default information in the {\sc tdfs}.  Thus
(\ref{tdfs}) can be represented as (\ref{abbtdfs}).
\begin{examples}
\item   \label{abbtdfs}
{\tiny $
\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{/b}}}\\ \attvaltyp{H}{a}}
$}
\end{examples}

The formal definition of {\sc tdfs}s is as follows:
\begin{defn}{\bf Typed Default Feature Structures}\\
A typed default feature structure defined on a set of features {\sf
Feat}, a type hierarchy $\langle\mbox{{\sf Type}},\sqsubseteq\rangle$
and a set of indices $N$ is a tuple $\langle {\cal T}, Q, {\cal R},
\delta,\theta\rangle$, where:
\begin{itemize}
\item   ${\cal T}$ is a tail: that is, it is a set of
pairs, where:
\begin{itemize}
\item   The first member of the pair is an atomic {\sc fs}, as defined
  in (Carpenter, 1993); \\ that is, a single path, or a path
equivalence; and
\item   the second member of the pair is a type;
\end{itemize}
\item   $Q$ is a finite set of nodes,
\item   ${\cal R} \in Q\times Q$ (these are the root nodes of the
indefeasible and defeasible {\sc tfs}s)
\item   $\theta: Q\longrightarrow \mbox{{\sf Type}}$ is a partial
typing function (this labels nodes with types).
\item   $\delta: Q\times \mbox{{\sf Feat}} \longrightarrow Q$ is a
partial feature value function.  
(This connects nodes with arcs labelled with features).\\
Note that for notational convenience we
may write a sequence of features $F_1\ldots F_k$ as $\pi$, and
$\delta(\ldots(\delta(n,F_1), F_2)\ldots F_k)$ as $\delta(n,\pi)$.)
\end{itemize}
Furthermore, the following must hold: if $\langle n_1,n_2\rangle =
{\cal R}$ then
\begin{enumerate}
\item   $n_1$ and $n_2$ aren't $\delta$-descendants.
\item   All members of $Q$ are $\delta$-descendants of $n_1$ or $n_2$
  (but not both).
\item There is no node $n$ or path $\pi$
such that $\delta(n,\pi) =n$.
\item   $\theta(n_2) \sqsubseteq \theta(n_1)$
\item   If $n\in Q$ is a $\delta$-descendant of $n_1$, 
and $\theta(n_2) \neq \bot$, then there is an isomorphic $m\in Q$ that
is a $\delta$-descendant of $n_2$.  That is:
\begin{enumerate}
\item   If $\delta(n,\pi) = n$, then 
$\delta(n_2,\pi) = m$; and
\item   $\theta(m)\sqsubseteq \theta(n)$
\end{enumerate}
(Conditions 1.~and 2.~ensure we have two separate
connected directed graphs.  Condition
3.~ensures these two directed graphs are acyclic.  And conditions 4.
and 5.~ensure defeasible information is at least as specific as
indefeasible information).
\end{enumerate}
\end{defn}

We can extract from any {\sc tdfs} the indefeasible {\sc tfs} $\langle
Q_I,n_1,\delta_I,\theta_I\rangle$, where $Q_I\subseteq Q$ are the
$\delta$-descendants of $n_1$, and $\delta_I$ and $\theta_I$ are the
projections of $\delta$ and $\theta$ onto $Q_I$; similarly for the
defeasible {\sc tfs}.  

\section{The Definition of YADU}
\label{informaldefn}

We now describe the operation {\sc yadu}, and we will prove that it
has the properties set out in section~\ref{intro} in
section~\ref{logic}.

The operation {\sc yadu}, which is notated $\ddunify$ and which
operates over {\sc tdfs}s, will be built up from a combination of the
unification and generalisation
operations $\unify$ and $\meet$ which operate on {\sc tfs}s (that is,
typed feature structures as defined in Carpenter (1992)).  So it is
necessary for us first to give a definition of these
operations on {\sc tfs}s.  We'll then show how together
with tails, they contribute to the definition of $\ddunify$ of {\sc
tdfs}s.

The
unification 
operation $\unify$ on {\sc tfs}s is defined here as in Carpenter
(1993), in terms of subsumption on typed feature structures.  First a
little notation: Let $F$ be a {\sc tfs}.  Then $\pi\equiv_{F}\pi'$
means that $F$ contains path equivalence or reentrancy between the
paths $\pi$ and $\pi'$; and ${\cal P}_F(\pi)=\sigma$ means that the
value on the path $\pi$ in $F$ is $\sigma$ (i.e, ${\cal
P}_F(\pi)=\sigma$ if and only if $\theta(\delta(n,\pi))=\sigma$, where
$n$ is the root node of $F$).  Subsumption is then defined as follows:
\begin{defn}
{\bf Subsumption of typed feature structures}\\
$F$ subsumes $F'$, written $F' \sqsubseteq F$, if and only if:
\begin{itemize}
\item $\pi \equiv_{F} \pi'$ implies $\pi \equiv_{F'} \pi'$
\item ${\cal P}_{F}(\pi) = t$ implies ${\cal P}_{F'}(\pi) = t'$ and $t' \sqsubseteq t$
\end{itemize}
\end{defn}
%
The subsumption hierarchy is a bounded complete partial order.

Unification is defined in terms of subsumption:
\begin{defn}{\bf Unification}\\
The unification $F \unify F'$ of two feature structures $F$ and $F'$
is taken to be the greatest lower bound of $F$ and $F'$ in the
collection of feature structures ordered by subsumption.
\end{defn}
%
Thus $F \unify F' = F''$ if and only if $F'' \sqsubseteq F$, $F''
\sqsubseteq F'$ and for every $F'''$ such that $F''' \sqsubseteq F$
and $F''' \sqsubseteq F'$ it is also the case that $F'''
\sqsubseteq F''$.  
Generalisation is the opposite of unification in which the lowest
upper bound of two feature structures is taken.  The generalisation of
two feature structures is defined to be the most specific feature
structure which contains only information found in both feature
structures.
%
\begin{defn}{\bf Generalisation}\\
The generalisation $F \generalize F'$ of two feature structures is
defined to be their greatest lower bound in the subsumption ordering.
\end{defn}
Thus $F \generalize F' = F''$ if and only if $F \sqsubseteq F''$, $F'
\sqsubseteq F''$ and for every $F'''$ such that $F \sqsubseteq F'''$
and $F' \sqsubseteq F'''$ then $F''
\sqsubseteq F'''$.

The operation {\sc yadu} on {\sc tdfs}s is defined in terms of an
extended version of Carpenter's (1993) credulous default unification,
which in turn is defined in terms of $\unify$ and $\meet$ on {\sc
tfs}s.  We extend it here, in that the second argument of the
operation will be a set of atomic {\sc tfs}s that may not be mutually
compatible, instead of it being a {\sc tfs}.

Carpenter's definition of credulous default unification is as follows:
\begin{defn}
\label{credulousdu}
{\bf Carpenter's Definition of Credulous Default Unification}\\ The
result of credulously adding the default information in $G$ to the
strict information in $F$ is given by:
\[
F\cunify G = \{ F\unify G': G'\sqsupseteq G \mbox{ is maximal such
that } F\unify G' \mbox{ is defined } \}
\]
\end{defn}
An example of the operation is given in Figure~\ref{creddu}.  One can
see that credulous default unification is asymmetric, and doesn't
return a single result deterministically.  So it doesn't meet the
criteria we specified in section~\ref{intro}.  However, defining
$\ddunify$ on {\sc tdfs}s in terms of $\cunify$ on {\sc tfs}s will
yield the properties we want.
We extend the definition of credulous default unification, so that it
takes a {\sc tfs} on the left hand side and a {\em set} of atomic {\sc
tfs}s on the right hand side, where these atomic {\sc tfs}s may 
contain mutually incompatible information:

\begin{figure}
Where $\mbox{{\bf t'}}\sqsubset \mbox{{\bf t}}$:

\begin{tabular}{llcc}
{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{a}\\ \attvaltyp{G}{{\boldmath
$\top$}}}$ }
\normalsize 
$ \dunify $ {\tiny $\avmplus{\att{t'}\\ \attval{F}{\ind{1}\
\myvaluebold{b}}\\ \attval{G}{\ind{1}}}$} & $=$ & {\tiny
$\left\{\avmplus{\att{t'}\\
\attvaltyp{F}{a}\\
                 \attvaltyp{G}{b}} ,
\avmplus{\att{t'}\\
\attval{F}{\ind{1}\ \myvaluebold{a}}\\
                 \attval{G}{\ind{1}}} \right\}$}
\end{tabular}
\caption{Credulous Default Unification}
\label{creddu}
\end{figure}


\[
\begin{array}{r l}
F_1 \cddunify \{G_1,\ldots,G_n\} = \{ F_1\unify F_2: & F_2 \mbox{ is
the unification of a maximal subset of }
\{G_1,\ldots,G_n\} \\
& \mbox{such that } F_1\unify F_2 \mbox{ is defined} \}
\end{array}
\]
We will want to iterate credulous default unification in what happens
below, and for this purpose, we define $\csddunify$ as follows:
\begin{defn}{\bf Credulous Default Unification $\csddunify$ on Sets}\\
Let ${\cal F}_1$ be a {\em set} of {\sc tfs}s $\{F_1,\ldots,F_n\}$,
and ${\cal G}_2$ a set of atomic {\sc tfs}s.  Then
\[
{\cal F}_1\csddunify{\cal G}_2 =
\{F_1\cddunify{\cal G}_2,\ldots,F_n\cddunify{\cal G}_2\}
\]
\end{defn}

The definition of $\ddunify$ will manipulate tails in a certain way,
and the following way of partitioning tails plays an important role in
defining how defaults behave under $\ddunify$:
\begin{defn}{\bf  The Specificity Partition of a Tail}\\
Let $T$ be a tail.  Then $\mu_1,\ldots\mu_m$ is a Specificity
Partition of $T$ if:
\[
T = \mu_1\cup\ldots \cup \mu_m
\]
and
\[
\begin{array}{r l l l}
\mu_1 = & \{\langle\phi,t\rangle\in T: & \forall\langle\phi',t'\rangle\in T,
t'\not\sqsubset t\} &\\
\mu_i = & \{\langle \phi,t\rangle \in T: & \exists \langle\phi',t'\rangle\in
\mu_{i-1} \mbox{ where }t'\sqsubset t \mbox{ and} & \\
&& \forall \langle\phi'',t''\rangle\in T\setminus
(\mu_1\cup\ldots\cup\mu_{i-1}), t''\not\sqsubset t\}& 2\leq i\leq m
\end{array}
\]
\end{defn}
Intuitively, $\mu_1$ is the
set of pairs in $T$ with the most specific types, $\mu_2$ is the
set of pairs in $T$ with the next most specific types, and so on.
Partitioning tails in order of specificity enables us to define
$\ddunify$ so that default information on more specific types
overrides that on more general types.  

We will also need to talk about the first and second members of the
pairs in the tail:
\begin{defn}{\bf Projection of Tails}\\
Let $T$ be a tail; i.e., a member of 
$\mbox{atomic {\sc fs}s}\times\mbox{{\sf Type}}$.  Then:
\[
\begin{array}{r l}
\wp_{fs}(T) = & \{\phi: \langle\phi,t\rangle\in T\}\mbox{ and}\\
\wp_{t}(T) = & \{t: \langle\phi,t\rangle\in T\}
\end{array}
\]
\end{defn}

Having set up this groundwork, we're now in a position to informally
define $\ddunify$ on {\sc tdfs}s in terms of $\meet$ and $\csddunify$
on {\sc tfs}s.  Let $F=_{def} I/D/T$ be a {\sc
tdfs}, and so $I$ is the indefeasible {\sc tfs}, $D$ the
defeasible {\sc tfs} and $T$ the tail.  Let
$F_1$ and $F_2$ be two {\sc tdfs}s, and let $F_{12}=_{def} F_1\ddunify
F_2$.  Furthermore, assume $F_{12}=_{def}
I_{12}/D_{12}/T^{12}$.  then $I_{12}$, $D_{12}$ and $T^{12}$ are 
calculated as follows:
\begin{enumerate}
\item   The Indefeasible Part:\\
$I_{12}= I_1\unify I_2$\\ That is, the indefeasible {\sc tfs} is the
unification of the indefeasible parts of the arguments.
\item   The Tail $T^{12}$:\\
$T^{12}=_{def} (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}$\\ where
$\mbox{{\em Bot}}^{12}$ are all the elements of $T^1\cup T^2$ where the
atomic {\sc fs} is incompatible with $I_{12}$.  That is:
\[
\mbox{{\em Bot}}^{12} = \{\langle F, \mbox{{\bf
t}}\rangle: \langle F,\mbox{{\bf t}}\rangle\in T^1\cup T^2 \mbox{ and
} F\unify I_{12}=\bot\}
\]

Note that if $I/D/T$ is a basic {\sc tdfs}, then its tail $T$ is defined
as follows:
\[
\begin{array}{r l}
T = \{ \langle \phi,t\rangle: & \mbox{where $t$ is the root type on
  $D$ and}\\
& \mbox{$\phi$ is an atomic {\sc fs} such that } 
\phi \sqsupseteq D \mbox{ but } \phi\not\sqsupseteq I\}
\end{array}
\]
\item   The Defeasible Part:
$D_{12}$ is defined in terms of $I_{12}$ and $T^{12}$.
We first divide $T^{12}$ into a specificity partition 
$\langle \mu_1,\ldots, \mu_n\rangle$.  Then
\[
D_{12}= \meet((I_{12} \csddunify \wp_{fs}(\mu_1))\csddunify
\ldots\csddunify \wp_{fs}(\mu_n))
\]
That is, $D_{12}$ is the generalisation of the `credulous default
unification' of: $I_{12}$; the atomic {\sc fs}s in $\mu_1$; \ldots; the
atomic {\sc fs}s in $\mu_m$, in that order.
\end{enumerate}

\subsection{Examples}

We will prove
that the operation has the
properties specified in section \ref{intro} in the
next section.  But first, we will
illustrate how the operation works by means of specific examples.

\subsubsection{Specificity}

The following example demonstrates that default reentrancies are
overridden by conflicting default information of a more specific type.
\begin{center}
Where $\mbox{{\bf t}}\sqsubset \mbox{{\bf t'}}$:

{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}\\ \attvaltyp{G}{/b}}$}
$\ddunify$
{\tiny $\avmplus{\att{t'}\\
  \attval{F}{/\ind{1}}\\ \attval{G}{/\ind{1}}} $}
\end{center}

\begin{itemize}
\item   $I_{12} = {\tiny \avmplus{\att{t}\\
                                \attval{F}{\top}\\ \attval{G}{\top}}}
\unify {\tiny \avmplus{\att{t'}\\
                                \attval{F}{\top}\\ \attval{G}{\top}}}
                            =
{\tiny \avmplus{\att{t}\\
                                \attval{F}{\top}\\ \attval{G}{\top}}}$
\item   $
\begin{array}[t]{l l l}
T^{12} & = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\ T^{1} & = &
\{\langle \mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}} \rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle\}\\
T^2 & = & \{\langle \mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\
\attval{G}{\ind{1}}}$}, \mbox{{\bf t'}}\rangle\}\\
\mbox{{\em Bot}}^{12} & = & \emptyset\\
\mbox{So}\\
T^{12} & = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\ & = &
\{\langle \mbox{\tiny
$\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}} \rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle, 
\langle \mbox{\tiny
$\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}, \mbox{{\bf
t'}}
\rangle\}
\end{array}
$

Therefore the specificity partition of $T^{12}$ is $\langle
\mu_1,\mu_2\rangle$, where:
\[
\begin{array}{r l}
\mu_1 = & \{\langle \mbox{\tiny
$\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}\rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle\}\\
\mu_2 = & \{\langle \mbox{\tiny
$\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}, \mbox{{\bf
t'}}\rangle\} 
\end{array}
\]
\item   
$
\begin{array}[t]{r l}
D_{12} = & \meet((I_{12} \csddunify \wp_{fs}(\mu_1)) \csddunify
\wp_{fs}(\mu_2))\\ = & \meet
\left(
\begin{array}{l}
\left(
\begin{array}{l}
\mbox{\tiny $\avmplus{\att{t}\\
        \attval{F}{\top}\\ \attval{G}{\top}}$}
\csddunify
\left\{
\begin{array}{l}
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},
\mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$}
\end{array}
\right\}
\end{array}
\right)
\csddunify
\mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\
        \attval{G}{\ind{1}}}$}
\end{array}
\right)\\
= & \meet
\left(
\begin{array}{l}
\mbox{\tiny 
$\avmplus{\att{t}\\ \attvaltyp{F}{a}\\ \attvaltyp{G}{b}}$}
\csddunify
\mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\
        \attval{G}{\ind{1}}}$}
\end{array}
\right)\\
= & \mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{a}\\
\attvaltyp{G}{b}}$}
\end{array}
$
\end{itemize}

Hence

$\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}\\ \attvaltyp{G}{/b}}$}
\ddunify
\mbox{\tiny $\avmplus{\att{t'}\\
  \attval{F}{/\ind{1}}\\ \attval{G}{/\ind{1}}}$} = 
\mbox{\tiny
$
\avmplus{\att{t}\\
\attvaltyp{F}{/a}\\
\attvaltyp{G}{/b}}$}
\left /
\begin{array}{l}
\{\langle \mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},t \rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},t\rangle, 
\langle \mbox{\tiny
$\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}, t'\rangle\}
\end{array}
\right.
$

\subsubsection{The Nixon Diamond}

The credulous unification operation $\csddunify$ doesn't generally
return a deterministic result.  However, $\ddunify$ does, even though
it's defined in terms of
$\csddunify$.  This is because
$\ddunify$ generalises over the
credulous options.
The following example
illustrates this.

\begin{center}
Where {\bf t} and {\bf t'} are in no specificity ordering, and
\[
\begin{array}{r l}
\mbox{{\bf t}} \unify \mbox{{\bf t'}} = & \mbox{{\bf t''}}\\
\mbox{{\bf a}}\unify \mbox{{\bf b}} = & \bot \\
\mbox{{\bf a}}\meet \mbox{{\bf b}}= & \mbox{{\bf c}}
\end{array}
\]

{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}\\ \attvaltyp{G}{/b}}$}
$\ddunify$
{\tiny $\avmplus{\att{t'}\\
  \attval{F}{/\ind{1}}\\ \attval{G}{/\ind{1}}} $}
\end{center}

\begin{itemize}
\item   $
\begin{array}[t]{r l}
I_{12} = & \mbox{\tiny $\avmplus{\att{t}\\
\                               \attval{F}{\top}\\
                                \attval{G}{\top}}$} \unify
\mbox{\tiny $\avmplus{\att{t'}\\
\                               \attval{F}{\top}\\
                                \attval{G}{\top}}$}\\ = & \mbox{\tiny
$\avmplus{\att{t''}\\ \attval{F}{\top}\\ \attval{G}{\top}}$}\\
\end{array}
$
\item   $
\begin{array}[t]{l l l}
T^{12} & = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\ T^{1} & = &
\{\langle \mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}} \rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle\}\\
T^2 & = & \{\langle \mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\
\attval{G}{\ind{1}}}$}, \mbox{{\bf t'}}\rangle\}\\
\mbox{{\em Bot}}^{12} & = & \emptyset\\
\mbox{So}\\
T^{12} & = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\ & = &
\{\langle \mbox{\tiny
$\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}\rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle, 
\langle \mbox{\tiny
$\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}, \mbox{{\bf 
t'}}\rangle\}
\end{array}
$

Therefore the specificity partition of $T^{12}$ is $T^{12}$ itself
(since both {\bf t} and {\bf t'} are the most specific types in
$T^{12}$).
\item   
$
\begin{array}[t]{r l}
D_{12} = & \meet((I_{12} \csddunify \wp_{fs}(T^{12})))\\ = &
\meet
\left(
\begin{array}{l}
\left(
\begin{array}{l}
\mbox{\tiny $\avmplus{\att{t''}\\
        \attval{F}{\top}\\ \attval{G}{\top}}$}
\csddunify
\left\{
\begin{array}{l}
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},
\mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},
\mbox{\tiny
 $\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}
\end{array}
\right\}
\end{array}
\right)
\end{array}
\right)\\
= & \meet
\left(
\begin{array}{l}
\left\{
\begin{array}{l}
\mbox{\tiny 
$\avmplus{\att{t''}\\ \attvaltyp{F}{a}\\ \attvaltyp{G}{b}}$},
\mbox{\tiny $\avmplus{\att{t''}\\
        \attvaltyp{F}{\mbox{$\ind{1}$}a}\\
\attvaltyp{G}{\mbox{$\ind{1}$}}}$},
\mbox{\tiny $\avmplus{\att{t''}\\
        \attvaltyp{F}{\mbox{$\ind{1}$}b}\\
\attvaltyp{G}{\mbox{$\ind{1}$}}}$}
\end{array}
\right\}
\end{array}
\right)\\
= & \mbox{\tiny $\avmplus{\att{t''}\\ \attvaltyp{F}{c}\\
\attvaltyp{G}{c}}$}
\end{array}
$
\end{itemize}

Hence

$\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}\\
\attvaltyp{G}{/b}}$}
\ddunify
\mbox{\tiny
$\avmplus{\att{t'}\\ \attval{F}{/\ind{1}}\\ \attval{G}{/\ind{1}}}$} =
\mbox{\tiny
$\avmplus{\att{t}\\
\attvaltyp{F}{/c}\\
\attvaltyp{G}{/c}}$}
\left /
\begin{array}{l}
\{\langle \mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}} \rangle,
\langle \mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t}}\rangle, 
\langle \mbox{\tiny
$\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}, \mbox{{\bf 
t'}}\rangle\}
\end{array}
\right.
$

\subsubsection{Well-Typed Unification}

Unlike the order independent typed default unification operation {\sc
  pdu} defined in Lascarides {\em et al.} (in press), $\ddunify$ never
produces {\sc tdfs}s where there is an atomic type/compound clash.
{\sc pdu} was problematic in that the following held:
\[
\begin{array}{l}
\mbox{Where {\bf t}}\sqsubset\mbox{{\bf t'} and {\bf a} is an atomic type:}\\
\\
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}}$} \mbox{{\sc pdu}}
\mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{/\avmplus{\att{t1}\\
        \attvaltyp{G}{b}}}}$} = 
\mbox{\tiny $\avmplus{\att{t}\\ \attval{F}{/\avmplus{\att{a\mbox{$\unify$}t1}\\
        \attvaltyp{G}{b}}}}$}
\end{array}
\]
So combining {\sc pdu}
with operations that ensure the result is always well-typed was not
investigated.  This problem with {\sc pdu} stemmed from the fact that
the defeasible
results of the operation for each path were calculated independently.
This made the operation polynomial, but produced odd results in cases
like those above.  In contrast, $\ddunify$ here is not calculated on a
path-by-path basis.  We'll demonstrate here that as a
consequence, we don't get atomic/compound clashes.  But the cost of
this is exponential complexity, since $\cunify$, on which $\ddunify$
is based, is exponential.

So, let's calculate the following:
\[
\begin{array}{l}
\mbox{Where {\bf t}}\sqsubset\mbox{{\bf t'}}\\
\\
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}}$} \ddunify
\mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{/\avmplus{\att{t1}\\
        \attvaltyp{G}{b}}}}$} 
\end{array}
\]

\begin{itemize}
\item   $\mbox{{\em I}}_{12} = \mbox{{\em I}}_1\unify \mbox{{\em I}}_2
  = \mbox{\tiny $\avmplus{\att{t}\\ \attval{F}{\top}}$}$
\item   
$
\begin{array}[t]{l l l}
T^{12}& = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\
T^1 & = & \{\langle\mbox{\tiny
  $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}\rangle\}\\
T^2 & = & \{\langle\mbox{\tiny
  $\avmplus{\attvaltyp{F}{t1}}$},\mbox{{\bf t'}}\rangle,
\langle\mbox{\tiny
  $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$},\mbox{{\bf t'}}
\rangle\}\\ 
\mbox{{\em Bot}}^{12} & = & \emptyset\\
\mbox{So}\\
T^{12}& = & (T^1\cup T^2)\setminus \mbox{{\em Bot}}^{12}\\
& = & \{\langle\mbox{\tiny
  $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}\rangle,
\langle\mbox{\tiny
  $\avmplus{\attvaltyp{F}{t1}}$},\mbox{{\bf t'}}\rangle,
\langle\mbox{\tiny
  $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$},\mbox{{\bf t'}}\rangle\}
\end{array}
$

Therefore the specificity partition of $T^{12}$ is $\langle
\mu_1,\mu_2\rangle$, where:
\[
\begin{array}{r l}
\mu_1 = & \{\langle \mbox{\tiny
  $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}\rangle\}\\
\mu_2 = & \{\langle
\mbox{\tiny
  $\avmplus{\attvaltyp{F}{t1}}$},\mbox{{\bf t'}}\rangle,
\langle\mbox{\tiny
  $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$},\mbox{{\bf
    t'}}\rangle\}
\end{array}
\]
\item   $
\begin{array}[t]{r l}
\mbox{{\em D}}_{12} = & \meet(((\mbox{{\em I}}_{12}\csddunify
\wp_{fs}(\mu_1)) \csddunify \wp_{fs}(\mu_2))\\
= & \meet
\left(
\begin{array}{c}
\left(
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\ \attval{F}{\top}}$} \csddunify 
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$}
\end{array}
\right\}
\end{array}
\right)
\csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{t1}}$},
\mbox{\tiny $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$}
\end{array}
\right\}
\end{array}
\right)\\
= &
\meet
\left(
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{a}}$} \csddunify 
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{t1}}$},
\mbox{\tiny $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$}
\end{array}
\right\}
\end{array}
\right)\\
= & 
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{a\mbox{$\unify$}t1}}$}
\end{array}
$
\end{itemize}

Hence
\[
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a}}$} \ddunify
\mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{/\avmplus{\att{t1}\\
        \attvaltyp{G}{b}}}}$} 
=
\mbox{\tiny $\avmplus{\att{t}\\ \attvaltyp{F}{/a\mbox{$\unify$}t1}}$}
\left/
\begin{array}{c}
\{
\langle
\mbox{\tiny
  $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t}}
\rangle,\langle
\mbox{\tiny
  $\avmplus{\attvaltyp{F}{t1}}$},\mbox{{\bf t'}}
\rangle,\langle
\mbox{\tiny
  $\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{b}}}}$},\mbox{{\bf t'}}
\rangle
\}
\end{array}
\right.
\]




\section{The Properties of $\ddunify$}
\label{logic}

We now demonstrate that $\ddunify$ has the desirable properties we
specified in section~\ref{intro}.  In what  follows, we use the
following notational convention: we refer to $F_1\ddunify F_2$ as
$F_{12}$, and $F_i=_{def} I_i/D_i/T^i$.

\begin{lemma}
\label{tailscomm}
Tails are commutative.
\end{lemma}


{\bf Proof}

This follows trivially, from the commutativity of $Bot^{12}$ and set
union.


\begin{lemma}
\label{tailsassoc}
Tails are associative.  That is: $T^{(12)3} = T^{1(23)}$
\end{lemma}

{\bf Proof}

\[
\begin{array}{r l}
T^{(12)3} = & (T^{12} \cup T^3)\setminus
Bot^{(12)3}\\ 
Bot^{(12)3} = & \{\langle F,t\rangle \in T^{12}
\cup T^3 \mbox{ such that {\em I}}_{(12)3}
\unify F = \bot\}\\
= & \{\langle F,t\rangle\in T^{12} \mbox{
  such that {\em I}}_{(12)3} \unify F=\bot\}\cup\\
& \{\langle F,t\rangle\in T^3 \mbox{ such that {\em
    I}}_{(12)3}\unify F=\bot\}
\end{array}
\]

Let $\langle F,t\rangle \in T^{(12)3}$.  Then:
\begin{examples}
\item [a] $\langle F,t\rangle\in T^{12}\setminus Bot^{(12)3}$; or
\item [b] $\langle F,t\rangle \in T^3\setminus Bot^{(12)3}$
\end{examples}
Suppose (b).  Then $\langle F,t\rangle\in T^3$ and $\mbox{{\em
    I}}_{(12)3}\unify F\neq \bot$.

Therefore,
$\langle F,t\rangle \in T^2\cup T^3$.
Furthermore, by the definition of typed unification,
$\mbox{{\em
    I}}_{(12)3} = \mbox{{\em I}}_{1(23)}\sqsubseteq \mbox{{\em
    I}}_{23}$.  
Therefore, since $\mbox{{\em I}}_{1(23)}\unify F\neq \bot$,
$\mbox{{\em
    I}}_{23}\unify F\neq\bot$.  So
$\langle F,t\rangle\in T^{23}$.
Furthermore,
$\mbox{{\em I}}_{1(23)}\unify F = \mbox{{\em I}}_{(12)3}\unify F\neq
\bot$. So $\langle F,t\rangle
\not\in Bot^{1(23)}$, and therefore
$\langle F,t\rangle\in T^{1(23)}$.

Now suppose (a) holds.  Then $\langle F,t\rangle \in ((T^1\cup
T^2)\setminus Bot^{12})\setminus Bot^{(12)3}$.  But
$Bot^{12}\subseteq Bot^{(12)3}$.  So either:
\begin{examples}
\item [i] $\langle F,t\rangle\in T^1\setminus
  Bot^{(12)3}$; or
\item [ii] $\langle F,t\rangle\in T^2\setminus  Bot^{(12)3}$
\end{examples}

Suppose (i) holds.  Then $\langle F,t\rangle\in T^1$
and $\mbox{{\em
       I}}_{(12)3}\unify F\neq \bot$.  So $\mbox{{\em I}}_{1(23)}\unify
   F\neq \bot$ by the order independence of typed unification.  So
   $\langle F,t\rangle \in T^1\setminus \mbox{{\em Bot}}^{1(23)} \subseteq
   T^{1(23)}$.

Suppose (ii) holds.  Then $\langle F,t\rangle \in T^2$ and $\mbox{{\em
    I}}_{(12)3}\unify F\neq\bot$.  So $\mbox{{\em I}}_{1(23)}\unify
F\neq \bot$, and therefore $\mbox{{\em I}}_{23}\unify F\neq \bot$.  So
$\langle F,t\rangle \not\in \mbox{{\em Bot}}^{23}$, and so $\langle
F,t\rangle \in T^{23}$.  Furthermore, since $\mbox{{\em
    I}}_{1(23)}\unify F\neq \bot$, $\langle
F,t\rangle\not\in\mbox{{\em Bot}}^{1(23)}$.  And so $\langle
F,t\rangle \in T^{1(23)}$.

So $T^{(12)3} \subseteq T^{1(23)}$.\\
By symmetry, $T^{1(23)}\subseteq T^{(12)3}$.  

Therefore $T^{1(23)} = T^{1(23)}$.   $\Box$

\begin{lemma}
\label{Rightarrowprops}
For any {\sc tdfs} $F=I/D/T$, $D=\bot$ or
\[
D = \meet((I\csddunify \wp_{fs}(\mu_1))\ldots
\wp_{fs}(\mu_m))
\]
Where $\langle\mu_1,\ldots,\mu_m\rangle$ is a specificity partition of
$T$.
\end{lemma}

{\bf Proof:} 
If $\mbox{{\em D}}=\bot$ we're done.  So we assume $\mbox{{\em
    D}}\neq \bot$.  Then there are two cases:
\begin{examples}
\item   [a]     The {\sc tdfs} {\sc f} is a basic {\sc tdfs}; or
\item   [b]     The {\sc tdfs} {\sc f} is a derived {\sc tdfs}.
\end{examples}

{\bf Case (a):} By the definition of basic tails and {\sc tdfs}s:
\[
\mbox{{\em D}}=\mbox{{\em I}}\unify\wp_{fs}(T)
\]
Furthermore, by the definition of basic tails, we know:
\begin{examples}
\item   [i]     $T$ is its own specificity partition;
\item   [ii]    since $\mbox{{\em D}}\neq \bot$,
  $\unify\wp_{fs}(T)\neq \bot$; and
\item   [iii]   $\forall F\in \wp_{fs}(T)$, $\mbox{{\em I}}\unify
  F\neq \bot$.
\end{examples}
So by the definition of $\meet$ and $\csddunify$:
\[
\mbox{{\em D}}=\mbox{{\em I}}\unify\wp_{fs}(T) =
\meet(\mbox{{\em I}}\csddunify \wp_{fs}(T))
\]

{\bf Case (b):} The result follows immediately by the definition of {\sc yadu},
given in section~\ref{informaldefn}. $\Box$.

\begin{lemma}
\label{yadufunction}
$\ddunify$ is a function.  That is $\mbox{{\sc tdfs}}_1\ddunify
\mbox{{\sc tdfs}}_2$ is a
unique {\sc tdfs}.
\end{lemma}

{\bf Proof :} 
The indefeasible {\sc tfs} of $\mbox{{\sc tdfs}}_1\ddunify \mbox{{\sc
    tdfs}}_2$ is unique because $\unify$ is deterministic.  The
tail is unique
because set union and $\unify$ are deterministic.  The specificity
partition of a tail is unique because the type hierarchy is a complete
partial order.  And so the
defeasible part of $\mbox{{\sc tdfs}}_1\ddunify \mbox{{\sc tdfs}}_2$
is unique because the specificity partion of a tail is unique and 
$\meet$ is deterministic.  $\Box$


\begin{lemma}
\label{yaducommutative}
$\ddunify$ is commutative.
\end{lemma}

{\bf Proof:}
Let us consider the $\ddunify$ of the {\sc tdfs}s $F_1$ and $F_2$.
The indefeasible part of $F_1\ddunify F_2$ is the same as the
indefeasible part of $F_2\ddunify F_1$ because $\unify$ is
commutative.  
The tails $T^{12}=T^{21}$ by lemma~\ref{tailscomm}.
And the defeasible part is defined in terms of the indefeasible part
and the tail.  But
$I_{12}= I_{21}$ and $T^{12} = T^{21}$ by lemma~\ref{tailscomm}.  So
$D_{12}= D_{21}$.  So $\ddunify$ is commutative. $\Box$


\begin{lemma}
\label{yaduassoc}
$\ddunify$ is associative.
\end{lemma}

{\bf Proof:} One needs to prove:
\begin{enumerate}
\item   $I_{(12)3} = I_{1(23)}$
\item   $D_{(12)3} = D_{1(23)}$
\item   $T^{(12)3} = T^{(12)3}$
\end{enumerate}
Case 1 follows immediately from the associativity of $\unify$.  Case 3 holds
by lemma~\ref{tailsassoc}.   Case 2 holds by
lemma~\ref{Rightarrowprops}: $D_{(12)3}$ is defined in terms of
$I_{(12)3}$ and
$T^{(12)3}$ which by cases 1 and 3 are the same as $\mbox{{\em
    I}}_{1(23)}$ and $T^{1(23)}$, and so $D_{(12)3}= D_{1(23)}$.
So $\ddunify$
is associative.  $\Box$

\begin{theorem}

$\ddunify$ is an order independent binary function.
\end{theorem}

{\bf Proof:} Follows immediately from
lemmas~\ref{yadufunction},~\ref{yaducommutative} and \ref{yaduassoc}.

The following theorem demonstrates that $\ddunify$ meets criterion 2
in 
section~\ref{intro}: $\ddunify$ reduces to $\unify$ when there's no conflict.

\begin{theorem}{\bf The Typed Unification Property}
\label{tup}
Let $F_1,F_2$ be {\sc tdfs}s.  And suppose
$I_{1\wedge 2}\unify\wp_{fs}(T^1)\unify\wp_{fs}(T^2)\neq \bot$.
Then $D_{1\wedge 2} = D_1\unify D_2$.
\end{theorem}

Before we prove this, note that theorem~\ref{tup} does
{\em not} specify that $\ddunify$ reduces to $\unify$ when
there's no conflict in the defeasible {\sc tfs}s.  This is because the
condition of the theorem is that $\mbox{{\em
    I}}_{12}\unify\wp_{fs}(T^1)\unify\wp_{fs}(T^2)\neq \bot$, and this
is a stronger condition than $\mbox{{\em D}}_1\unify\mbox{{\em
    D}}_2\neq \bot$.  The result deson't hold for the latter condition
alone, as the following example demonstrates:

Where
\[
\begin{array}{l}
\mbox{{\bf t1}}\sqsubset \mbox{{\bf t2}}\sqsubset \mbox{{\bf
    t3}}\\
\mbox{{\bf a}}\unify \mbox{{\bf c}}= \bot\\
\mbox{{\bf b}}\unify \mbox{{\bf c}}=\bot\\
\mbox{{\bf a}}\meet \mbox{{\bf b}} = \top
\end{array}
\]

\[
\mbox{\tiny $\avmplus{\att{t1}\\ \attval{F}{/\ind{1}}\\
                \attval{G}{/\ind{1}}}$}
\left/
\begin{array}{c}
\{
\langle
\mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$},
\mbox{{\bf t1}}
\rangle,\langle
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$},\mbox{{\bf t2}}
\rangle,\langle
\mbox{\tiny $\avmplus{\attvaltyp{G}{b}}$},\mbox{{\bf t2}}
\rangle\}
\end{array}
\right.
\ddunify
\mbox{\tiny $\avmplus{\att{t3}\\ \attvaltyp{F}{/c}\\
    \attval{G}{\top}}$}
\left/
\begin{array}{c}
\{
\langle
\mbox{\tiny $\avmplus{\attvaltyp{F}{c}}$},\mbox{{\bf t3}}
\rangle
\}
\end{array}
\right.
\]

We just show how to calculate the defeasible {\sc tfs}:
\[
\begin{array}{r l}
\mbox{{\em D}}_{12} = & 
\meet
\left(
\begin{array}{c}
\left(
\begin{array}{c}
\left(
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{\top}\\
    \attval{G}{\top}}$} \csddunify 
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attval{F}{\ind{1}}\\ \attval{G}{\ind{1}}}$}
\end{array}
\right\}
\end{array}
\right)
\csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$}, \mbox{\tiny
  $\avmplus{\attvaltyp{G}{b}}$} 
\end{array}
\right\}
\end{array}
\right)
\csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{c}}$}
\end{array}
\right\}
\end{array}
\right)\\
= &
\meet
\left(
\begin{array}{c}
\left(
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{\ind{1}}\\
    \attval{G}{\ind{1}}}$} \csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{a}}$}, \mbox{\tiny
  $\avmplus{\attvaltyp{G}{b}}$} 
\end{array}
\right\}
\end{array}
\right)
\csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{c}}$}
\end{array}
\right\}
\end{array}
\right)\\
= & 
\meet
\left(
\begin{array}{c}
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t'}\\ \attvaltyp{F}{\mbox{$\ind{1}$}a}\\
    \attval{G}{\ind{1}}}$}, 
\mbox{\tiny $\avmplus{\att{t'}\\ \attvaltyp{F}{\mbox{$\ind{1}$}b}\\
    \attval{G}{\ind{1}}}$}
\end{array}
\right\}
\csddunify
\left\{
\begin{array}{c}
\mbox{\tiny $\avmplus{\attvaltyp{F}{c}}$}
\end{array}
\right\}
\end{array}
\right)\\
= & 
\mbox{\tiny $\avmplus{\att{t'}\\ \attvaltyp{F}{\mbox{$\ind{1}$}a}\\
    \attval{G}{\ind{1}}}$} \meet
\mbox{\tiny $\avmplus{\att{t'}\\ \attvaltyp{F}{\mbox{$\ind{1}$}b}\\
    \attval{G}{\ind{1}}}$}\\
= & \mbox{\tiny $\avmplus{\att{t'}\\ \attval{F}{\ind{1}}\\
    \attval{G}{\ind{1}}}$} 
\end{array}
\]

Thus $\mbox{{\em D}}_{12}\neq \mbox{{\em D}}_1\unify \mbox{{\em D}}_2$
in this case, even though 
\[
\mbox{{\em D}}_1\unify\mbox{{\em D}}_2 = \mbox{\tiny
  $\avmplus{\att{t'} \\ \attvaltyp{F}{\mbox{$\ind{1}$}c}\\
    \attval{G}{\ind{1}}}$} \neq \bot
\]


{\bf Proof of Theorem~\ref{tup}:}\\


$T^{12} = T^1\cup T^2$, because $\mbox{{\em I}}_{12}\unify  \wp_1(T^1)
\neq \bot$, and $\mbox{{\em I}}_{12}\unify \wp_1(T^2)\neq \bot$.  

Let $\mu_1\ldots\mu_n$ be a Specificity Partition Tail of $T^{12}$.  Then
by lemma~\ref{Rightarrowprops}:
\[
\mbox{{\em D}}_{12} =  \meet(\mbox{{\em I}}_{12} \csddunify
\wp_{fs}(\mu_1)\csddunify \ldots \csddunify \wp_{fs}(\mu_n))
\]
But by assumption $\mbox{{\em I}}_{12}\unify\wp_{fs}(\mu_1) \neq\bot$.
So by the definition of $\csddunify$:
\[
\mbox{{\em I}}_{12}\csddunify \wp_{fs}(\mu_1) = \mbox{{\em
    I}}_{12}\unify\wp_{fs}(\mu_1) \neq\bot
\]
Similarly $(\mbox{{\em
    I}}_{12}\unify \wp_{fs}(\mu_1)) \unify \wp_{fs}(\mu_2)\neq \bot$.
So by the definition of $\csddunify$:
\[
((\mbox{{\em I}}_{12}\csddunify \wp_{fs}(\mu_1)) \csddunify
\wp_{fs}(\mu_2) = \mbox{{\em I}}_{12} \unify \wp_{fs}(\mu_1) \unify
\wp_{fs}(\mu_2)
\]
By similar arguments for $\mu_3,\ldots,\mu_n$:
\[
\begin{array}{r l}
\mbox{{\em D}}_{12} = &
\meet((\mbox{{\em I}}_{12}\csddunify \wp_{fs}(\mu_1))\ldots \csddunify
\wp_{fs}(\mu_n))\\
= &
\meet(\mbox{{\em I}}_{12}\unify \wp_{fs}(\mu_1)\unify\ldots\unify
\wp_{fs}(\mu_n))\\ 
= & \mbox{{\em I}}_{12}\unify \wp_{fs}(T^{12})\\
= & \mbox{{\em I}}_1\unify \wp_{fs}(T^1) \unify \mbox{{\em I}}_2\unify
\wp_{fs}(T^2) 
\end{array}
\]
By a similar argument to that above:
\[
\begin{array}{r l}
\mbox{{\em D}}_1 = & \mbox{{\em I}}_1 \unify \wp_1(T^1)\\
\mbox{{\em D}}_2 = & \mbox{{\em I}}_2 \unify \wp_1(T^2)
\end{array}
\]
So
\[
\mbox{{\em D}}_{12} = \mbox{{\em D}}_1 \unify \mbox{{\em D}}_2
\]
as required. $\Box$

Because {\sc tdfs}s contain more information than the information in
the {\sc fs} components alone, the notion of `conflict' is more
complex than in Carpenter (1992, 1993) and Bouma (1992).  Their
definitions of default unification correspond to the situations where
we are unifying structures in the initial {\sc kb}---that is, basic
{\sc tdfs}s.  and we can prove that for these cases the typed
unification property is one where $\ddunify$ reduces to $\unify$ when
there is no conflict among the {\sc fs} components:

\begin{corollary}{\bf The Typed Unification Property for Basic {\sc
      tdfs}s}\\
\label{tupbasic}
If {\sc tdfs}$_1$ and {\sc tdfs}$_2$ are basic {\sc tdfs}s, and
$D_1\unify D_2\neq \bot$, then 
\[
D_{12}= D_1\unify D_2
\]
\end{corollary}

{\bf Proof:}
Since {\sc tdfs}$_1$ and {\sc tdfs}$_2$ are basic:
$\mbox{{\em D}}_i = \mbox{{\em I}}_i\unify \wp_{fs}(T^i)$ for $i =
1,2$.  So, since $\mbox{{\em D}}_1\unify \mbox{{\em D}}_2\neq \bot$:
\[
\begin{array}{r l}
\mbox{{\em I}}_1\unify \wp_{fs}(T^1) \unify \mbox{{\em I}}_2\unify
\wp_{fs}(T^2) = & \mbox{{\em I}}_{12} \unify \wp_{fs}(T^1) \unify
\wp_{fs}(T^2)\\ 
\neq & \bot
\end{array}
\]
So by theorem~\ref{tup}:
\[
\mbox{{\em D}}_{12} = \mbox{{\em D}}_1\unify \mbox{{\em D}}_2
\]
$\Box$



\section{Conclusion}

We have defined a version of default unification on typed feature
structures which is both
order independent and sufficiently expressive to allow overriding of
any default information by more specific conflicting defaults.
This has numerous potential applications in computational linguistics,
both in improving the declarativity of existing uses of default
inheritance within the lexicon, and allowing defaults to persist beyond the
lexicon (Lascarides {\em et al}, in press).
The worst-case complexity properties of {\sc yadu} are unpromising
since it involves multiple applications of
Carpenter's credulous default unification operation, which is apparently
NP-complete.  Many applications 
involve rather few default statements, however, and if these
tend not to interact, the operation won't be intractable in practice.  
In future work, we will demonstrate the utility of {\sc yadu} in
several linguistic applications.


\section*{References}

\newcommand{\book}[4]{\item #1 (#4) {\it #2,} #3.}
\newcommand{\booknoauthor}[3]{\item #1 (#3) {\it #2,}}
\newcommand{\forthedbook}[4]{\item #1 (eds.) (#4, forthcoming) {\it #2,} #3.}
\newcommand{\unpub}[4]{\item #1 (#4) {\it #2,} #3.}
\newcommand{\bookart}[7]{\item #1 (#7) `#2' in #5 (eds.), {\it #4,} #6, pp.~#3.}
\newcommand{\bookartnopp}[6]{\item #1 (#6) `#2' in #4 (eds.), {\it #3,} #5.}
\newcommand{\forthart}[6]{\item #1 (#6, forthcoming) `#2' in #4 (eds.),
{\it #3,} #5.}
\newcommand{\journart}[6]{\item #1 (#6) `#2', {\it #3,} {\it vol.#4,}
#5.}
\newcommand{\journartnopp}[5]{\item #1 (#5) `#2', {\it #3,} {\it vol.#4,}}
\newcommand{\forthjournart}[4]{\item #1 (#4) `#2', {\it #3,}}
\newcommand{\procart}[6]{\item #1 (#6) `#2', {\it Proceedings of the
#3,} #4, pp.~#5.}
\newcommand{\forthprocart}[5]{\item #1 (#5) `#2', 
to appear in {\it Proceedings of the #3,} #4}
\newcommand{\procartnopp}[5]{\item #1 (#5) `#2', {\it Proceedings of the
#3,} #4.}

\begin{list}{}
   {\leftmargin 1.6em
    \itemindent -\leftmargin
    \itemsep 0pt plus 1pt
    \parsep 0pt plus 1pt}

\procart{Asher, N. and Morreau, M.}
        {Common Sense Entailment: A Modal Theory of Nonmonotonic
          Reasoning}
        {Proceedings of the 12th International Joint Conference on
          Artificial Intelligence}
        {Sydney Australia}
        {}
        {1991}

\bookartnopp{Blackburn, P.}
{Modal Logic and Attribute Value Structures}
{Diamonds and Defaults}
{M.~de~Rijke}
{Studies in Logic, Language and Information. Kluwer, Dordrecht,
Holland (available as University of Amsterdam, ITLI, LP-92-02)} 
{1992}

\procart{Boguraev, B. and J.~Pustejovsky}
        {Lexical ambiguity and the role of knowledge representation in
lexicon design}
        {13th Int. Conf. on Comp. Ling. (COLING-90)}
        {Helsinki}
        {36--42} 
        {1990}

\journart{Bouma, G.}
         {Feature structures and nonmonotonicity}
         {Computational Linguistics}
         {18.2}
         {183--204}
         {1992}

\procart{Briscoe, E.J., A.~Copestake and B.K.~Boguraev}
    {Enjoy the paper: Lexical semantics via lexicology}
    {13th Int. Conf. on Comp. Ling. (COLING-90)}
    {Helsinki}
    {42--47} 
    {1990}


\book{Carpenter, R.}
{The logic of typed feature structures}
{(Tracts in Theoretical Computer Science), Cambridge University Press,
  Cambridge, England} 
{1992}

\bookart{Carpenter, R.}
           {Skeptical and credulous default unification with
application to templates and inheritance}
    {13--37}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\book{Copestake, A.}
{The Representation of Lexical Semantic Information}
{Doctoral dissertation, University of Sussex,
Cognitive Science Research Paper CSRP 280}
{1992}

\bookart{Copestake, A.}
    {Defaults in lexical representation}
    {223--245}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\procart{Daelemans, W.}
        {A tool for the automatic creation, extension and updating of
lexical knowledge bases}
{3rd Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-87)}
        {Copenhagen}
        {70--74}
        {1987}


\journart{Daelemans, W., K.~de Smedt and G.~Gazdar}
         {Inheritance in natural language processing}
         {Computational Linguistics}
         {18.2}
         {205--218}
         {1992}

\procart{Evans, R. and G.~Gazdar}
{Inference in DATR}
{4th Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-1989)}
{Manchester,  England}
{66--71}
{1989a}

\bookart{Evans, R. and G.~Gazdar}
{The semantics of DATR}
{79--87}
{Proceedings of the Seventh Conference of
  the Society for the Study of Artificial Intelligence and Simulation of
  Behavior (AISB)}
{A.~G.~Cohn}
{Pitman/Morgan Kaufmann, London}
{1989b}

\unpub{Flickinger,  D.}
        {Lexical Rules in the Hierarchical Lexicon}
        {PhD thesis, Stanford University} 
        {1987}


\procart{Flickinger, D., C.~Pollard and T.~Wasow}
        {Structure sharing in lexical representation}
        {23rd Annual Meeting of the Association for Computational
        Linguistics (ACL-85)}
        {University of Chicago}
        {262--268}
        {1985} 



\journart{Flickinger, D. and J.~Nerbonne}
{Inheritance and complementation: A case study of {\it easy}
adjectives and related nouns}
         {Computational Linguistics}
         {18.3}
         {269--310}
         {1992}


\journart{Hayes, B.}
{Inalterability in CV Phonology}
{Language}
{62 (2)}
{pp321--351}
{1986}

\bookart{Kaplan, R.}
  {Three seductions of computational psycholinguistics}
  {149--188}
  {Linguistic Theory and Computer Applications}
  {P.~Whitelock, H.~Somers, P.~Bennett, R.~Johnson, and M.~McGee Wood}
  {Academic Press, London}
  {1987}

\procart{Kasper, R.~T. and  W.~C. Rounds}
{A logical semantics for feature structures}
{24th Annual Conference of the Association for Computational
Linguistics}
{Columbia University}
{235--242}
{1986}


\bookart{Kreiger, H. and J.~Nerbonne}
    {Feature-based inheritance networks for computational lexicons}
    {90--136}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\procartnopp{Lascarides, A. and A.~Copestake}
{The Pragmatics of Word Meaning}
{Semantics and Linguistic Theory (SALT5)}
{University of Texas at Austin}
{1995}


\journart{Lascarides, A. and N.~Asher}
{Temporal Interpretation, Discourse Relations and Common Sense Entailment}
{Linguistics and Philosophy}
{16}
{437--493}
{1993}


\forthjournart{Lascarides, A., E.J.~Briscoe, N.~Asher and
A.~Copestake}
{Order Independent and Persistent Typed Default Unification}
{Linguistics and Philosophy}
{in press}

\journart{Reiter, R.}
{A Logic for Default Reasoning}
{Artificial Intelligence}
{13}
{81--132}
{1980}

\procart{Russell, G., J.~Carroll and  S.~Warwick}
{Multiple default
inheritance in a unification-based lexicon} 
{29th Annual Meeting of the Association for Computational 
Linguistics (ACL-91)}
{Berkeley, California}
{215--221}
{1991}

\book{Shieber, S.~M.}
{An introduction to unification-based approaches to grammar}
{CSLI Lecture Notes 4, Stanford CA}
{1986}

\bookart{Vossen, P. and A.~Copestake}
    {Untangling definition structure into knowledge representation}
    {246--274}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}


\procart{Young, M. and W.~Rounds}
        {A logical semantics for nonmonotonic sorts}
        {31st Annual Meeting of the Association for 
Computational Linguistics (ACL-93)}
        {Columbus, Ohio}
        {209--215}
        {1993}

\end{list}



\end{document}






