\documentstyle[12pt,a4j,proof]{article}

% --- LAYOUT SETTING ---
\textwidth=5.5in
\textheight=7.5in
\topmargin=0.2in
\oddsidemargin=0.3in
\normalbaselineskip=15pt
% ----------------------

\begin{document}
%\pagestyle{empty}
\setcounter{page}{1}
\font\title=cmr10
\normalbaselines
\begin{center}
\large{\bf A Labelled Deductive Approach to DRT II:}
\large{\bf Reasoning with DRSs as Information Structures}
\end{center}
\smallskip
\centerline{\bf Seiki Akama}
\centerline{\bf Michio Kobayashi}
\centerline{Computational Logic Laboratory, Department of Information Systems,}
\centerline{Teikyo Heisei University, 2289 Uruido, Ichihara-shi, }
\centerline{Chiba, 290-01, Japan. }
\centerline{e-mail: SJK15022@mgw.shijokyo.or.jp }
\bigskip

\centerline{This paper is submitted to \bf{ITALC'96. }\rm}
\bigskip
\centerline{December 27, 1995.}
\bigskip
\noindent
\bf{Abstract}\rm\par\noindent
We explore a deduction mechanism in Discourse Representation Theory (DRT) with
in Gabbay's Labelled Deductive System (LDS). We formulate a labelled natural 
deduction system capable of manipulating DRSs. It is then possible to deal 
with  various inferences in discourse by regarding DRSs as information 
structures. 
 \par

\bigskip\noindent
%\bf{Topic Area }\rm \par\noindent
%Discourse, Discourse Representation Theory. \par
%\bigskip

\noindent{\bf 1. Introduction} \rm\par\noindent
\it{Discourse Representation Theory }\rm (DRT) is one of the promising 
frameworks for natural language discourse; see Asher (1993) and Kamp and Ryle 
(1993).  Although DRT offers the solution of some issues in discourse 
semantics, it should be further elaborated for wider applications. 
For this purpose, we need to work out an inference system for DRT. 
Saurer (1991) presented a natural deduciton system for DRT, but it is not 
satisfactory for computational linguistics and knowledge representation; also 
see Akama and Nakayama (1991, 1993). \par

        In Akama and Kobayashi (1995), we described DRT within the framework 
of Gabbay's (1993, 1996) \it{Labelled Deductive System }\rm (LDS) for giving a
proof-theoretic description of Asher's bottom up construction of DRSs.  But we
 have not dealt with deduction with DRSs in the proposed formulation. Recently,
 Reyle and Gabbay (1994) outlined direct deductive computation on DRSs 
inspired by the computation procedure of N-Prolog. \par
 
        This paper sketches a LDS formulation of reasoning with DRSs by 
providing a labelled natural deduction system $LND$. The point in our 
formalization is to view DRSs as informaion structures for accommodating 
various inferences in discourse in a uniform way. \par

\bigskip

\noindent{\bf 2. Labelled Natural Deduction System for DRT}\rm\par
\noindent
In Akama and Kobayashi (1995), we showed an algorithmic proof method for 
Asher's (1993) semantics for the DRS construction procedure in the setting of 
Gabbay's LDS. It is thus possible to dualize the parsing and construction of 
the DRSs from a discourse. The next task is to develop a proof procedure for 
the manipulation of DRSs, i.e. reasoning with DRSs. This can be also given by 
identifying DRSs with labelled formulas. Additionally, we address the nature 
of DRSs as information structures. One attractive way is to generalize 
\it{natural deduction }\rm (cf. Prawitz (1965)) as \it{labelled natural 
deduction. }\rm This idea is not novel. In fact, it was already considered in 
the literature on the proof theory for relevant logics in 1970's. \par

        Following Asher (1993), a \it{predicative }\rm DRS is of the form 
$\lambda x_{1} ... \lambda x_{n} \langle U_{K} - \lbrace x_{1},..., x_{n} 
\rbrace, Con_{K}(x_{1},..., x_{n}) \rangle$, which corresponds to a common 
noun or a verb.  A \it{partial }\rm DRS is a translation of a determiner or a 
proper name.  A \it{DRS-conversion }\rm is a DR-theoretic generalization of 
$\beta$-conversion in $\lambda$-calculus.  \par

        We define a labelled formulas as a pair, namely $DRS:$ (type of 
embedding function). In this regard, DRSs can be handled by a functional 
interpretation inherited in $\lambda$-calculus. We use the type $\tau_{0}$ for
 a predicative DRS as a primitive type. Any type employed in DRT can be 
constructed from the basic type. \par

        Recall that the language of DRT contains the logical connectives: 
$\Rightarrow, \vee$, and $\neg$. Conjunction is implicit in the set of 
conditions in a DRS. Thus, we need rules for these connectives. Here are rules
 for $LND$:
 \par
\smallskip
\ \ \ \ \ $\infer[(+I)]{K_{1} + K_{2}: t}{K_{1}: t & K_{2}: t}$ \par
\ \ \ \ \ $\infer{K_{1}: t}{K_{1} + K_{2}: t}$ \ \ 
$\infer[(+E)]{K_{2}: t}{K_{1} + K_{2}: t}$ \par\smallskip
\ \ \ \ \ $\infer{K_{1} \vee K_{2}: t}{K_{1}: t}$ \ \ \ 
$\infer[(\vee I)]{K_{1} \vee K_{2}: t}{K_{2}: t}$ \par\smallskip
\ \ \ \ \ $\infer[(\vee E)]{K_{3}: t}{K_{1} \vee K_{2}: t 
& \deduce{K_{3}: t}{[K_{1}: t]} & \deduce{K_{3}: t}{[K_{2}: t]}}$ \par
\ \ \ \ \ $\infer[(\Rightarrow I)]{K_{1} \Rightarrow K_{2}: t}
{\deduce{K_{2}: t}{[K_{1}: t]}}$ \par\smallskip
\ \ \ \ \ $\infer[(\Rightarrow E)]{K_{2}: t}
{K_{1}: t & K_{1} \Rightarrow K_{2}: t}$ \par
\ \ \ \ \ $\infer[(false)]{K: t}{false: t}$ \ \ \ $\infer[(RAA)]{K: t}
{\neg\neg K: t}$ \par
\smallskip\noindent
Here, the assumed DRSs in the bracket in $(\vee E)$ and $(\Rightarrow I)$ are 
\it{discharged }\rm (cf. Prawitz (1965)), and $false$ denotes a DRS 
$\langle \lbrace \ \rbrace, \lbrace \ \rbrace \rangle$ for absurdity. Negation
 $\neg K$ is an abbreviation for $K \Rightarrow false$. In addition, we need 
the following two rules for type inferences. \par

\smallskip
\ \ \ \ \ $\infer[(\rightarrow I)]
{\lambda x^{A}.\alpha(x^{A}): A \rightarrow B}{\alpha(x^{A}): B}$ 
\par\smallskip
\ \ \ \ \ $\infer[(\rightarrow E)]{\alpha (\beta): B}
{\alpha: A \rightarrow B & \beta: A}$ \par\smallskip\noindent
This version of $LND$ supports classical logic. If we want to base 
intuitionistic logic, $(RAA)$ should be given up. The proposed natural 
deduction system has a label for expressing the type of embedding function. In
 this regard, it is closely related to a calculus for type theory. 
\par\noindent
\bf{Example 1}\rm\par\noindent
John walks. He whistles. \par\noindent
\ \ \ Then, John whistles. \par\noindent
First, the premises translate into DRSs by means of Asher's bottom up DRS 
construction (cf. Akama and Kobayashi (1995)): \par
        John \ $\Rightarrow$ \ $\lambda P \langle \lbrace x \rbrace, \lbrace 
John(x), P(x) \rbrace \rangle: \tau_{0} \rightarrow \tau_{0}$  \par
        walks \ $\Rightarrow$ \ $\lambda x \langle \lbrace \ \rbrace, \lbrace 
walk(x) \rbrace \rangle: \tau_{0}$  \par
        John walks $(K_{1})$ \ $\Rightarrow$ \ $\lambda x \langle \lbrace x 
\rbrace, \lbrace John(x), walk(x) \rbrace \rangle: \tau_{0}$  \par
        he \ $\Rightarrow$ \ $\lambda P \langle \lbrace y \rbrace, \lbrace P(y)
, y = ? \rbrace \rangle: \tau_{0} \rightarrow \tau_{0}$  \par
        He whistles \ $\Rightarrow$ \ $\langle \lbrace y \rbrace, \lbrace 
whistle(y), y = ? \rbrace \rangle: \tau_{0}$ \par\noindent
The first sentence is updated by the second using $(+I)$ to yield 
$K_{1} + K_{2}$: \par
        $\langle \lbrace x, y \rbrace, \lbrace John(x), walk(x), whistle(y), y
 = x \rbrace \rangle: \tau_{0}$ \par\noindent
Here, the incomplete condition can be fixed since $y$ is accessible to $x$. 
Thus, by $(+E)$ we have $K_{2}: \tau_{0}$, namely \par
        $\langle \lbrace x,y \rbrace, \lbrace whistle(y), y = x \rbrace 
\rangle: \tau_{0}$ \par\noindent
to conclude that John whistles. \par

\bigskip

\noindent{\bf 3. DRSs as Information Structures}\rm\par
\noindent
In the previous section, we have shown that the proposed labelled natural 
deduction system enables us to deduce the appropriate DRS from a given DRS. Fo
r 
instance, Example 1 is concerned with the reasoning about anaphora resolution.
 
The mechanism is triggered according to the condition (i.e. accessibility) on 
DRSs. It is, however, to desirable to incorporate such a mechanism into the 
deduction system. One way to establish it is to add the rule with additional 
label. Let $K[y = ?]$ be a DRS containing the incomplete condition $y = ?$. We
 
denote $y \sim x$ to express that $y$ is accessible to $x$. Below we employ th
e 
notation as the second label. Using these notions, we can axiomatically deal 
with anaphora resolution in $LND$. For this purpose, we add the following rule
: 
\par
\smallskip
\ \ \ \ \ $\infer[(ASUB)]{K[P(y)]: t}{K[P(x)]: t, y \sim x}$ \par\noindent
which reads ``if a DRS $K$ contains the condition $P(x)$ and $y$ is accessible
 to $x$, then $x$ in $P$ can be replaced by $y$ to yield $P(y)$". Using $(ASUB)
$, we can reanalyze example 1: \par\noindent
\bf{Example 2}\rm\par\noindent
John walks. He whistles. \par
        By the DRS construction procedure and updating, we have the following 
incomplete DRS: \par
        $\langle \lbrace x, y \rbrace, \lbrace John(x), walk(x), whistle(y), y
 = ? \rbrace \rangle: \tau_{0}$ \par\noindent
where $x$ and $y$ are in the same universe. It is thus possible to add a label
 for accessibility: \par
        $\langle \lbrace x, y \rbrace, \lbrace John(x), walk(x), whistle(y), y
 = ? \rbrace \rangle: \tau_{0}, x \sim y$ \par\noindent
Then, $(ASUB)$ can infer: \par
        $\langle \lbrace x, y \rbrace, \lbrace John(x), walk(x), whistle(y), y
 = x \rbrace \rangle: \tau_{0}, x \sim y$ \par\noindent
By $(+E)$, the same conclusion follows as in Example 1. \par
        However, it may not be the case that we cannot properly perform 
anaphora resolution from the available information. \par\noindent
\bf{Example 3 }\rm\par\noindent
A professor supervized a Ph. D. student. He failed to complete a dissertation.
 He stopped to study the subject. \par
        The discourse consists of the following three DRSs, ie. $K_{1}, K_{2}$
 and $K_{3}$: \par\noindent
$K_{1}$: $\langle \lbrace x, y \rbrace, \lbrace professor(x), phd\_student(y),
 supervize(x, y) \rbrace \rangle: \tau_{0}$ \par\noindent
$K_{2}$: $\langle \lbrace z \rbrace, \lbrace fail(z), z = ? \rbrace: \tau_{0}$
 \par\noindent
$K_{3}$: $\langle \lbrace u \rbrace, \lbrace \neg study(u), z = ? \rbrace: 
\tau_{0}$ \par

        First, $K_{1}$ is updated by $K_{2}$. \par\noindent
$K_{1} + K_{2}$: $\langle \lbrace x, y, z \rbrace, \lbrace professor(x), 
phd\_student(y), supervize(x, y), fail(z), z = ? \rbrace \rangle: \tau_{0}, 
z \sim y$ \par

        The information about accessibility can move to: \par\noindent
\ \ \ $\langle \lbrace x, y, z \rbrace, \lbrace professor(x), phd\_student(y),
 supervize(x, y), fail(z), z = y \rbrace \rangle: \tau_{0}, z \sim y$ 
\par\noindent
Here, the common-sense that a student, not a professor, writes a Ph. D. 
dissertation enables the anaphora resolution, although $z$ is accessible to $x
$ 
and $y$. Note that there is no DR-theoretic account on the reasoning unless we
 
have extra information like a gender. Next, the new information is supplied by
 
$K_{3}$: \par\noindent
$K_{1} + K_{2} + K_{3}$: $\langle \lbrace x, y, z, u \rbrace, \lbrace 
professor(x), phd\_student(y), supervize(x, y)$, \par\noindent
$fail(z), z = y, \neg study(u), u = ? \rbrace \rangle: \tau_{0}, z \sim y, u 
\sim y \sim x$ \par
        It is here difficult to determine a correct antecedent of $u$, because
 $z$ is accessible to both $x$ and $y$. There are two possible interpretations.
 One is that the Ph.D. student stopped to study the subject due to the failure
 of completing a dissertation. The other is that the professor stopped to 
study the subject which is central to his student's thesis. How should we 
determine it?   \par

        One of the attractive ideas is to introduce defaults into DRT allowing
 for the so-called \it{non-monotonic reasoning. }\rm  Asher (1991) advanced a 
belief revision model to deal with non-monotonic reasoning in DRT. Asher's for
malization can be directly incorporated into our framework. We here address 
the importance of default aspects of discourse semantics. For instance, we can
 
strengthen $(ASUB)$ with the default features as follows: \par
\ \ \ $\infer[(DASUB)]{K[P(y))]: t}{K[P(x)]: t, y \sim x & M(K[P(y)]: t}$ \par
\noindent
where $M$ is something like a \it{consistency operator }\rm in non-monotonic 
logics. In this regard, $(DASUB)$ can accommodate non-monotonic reasoning in 
DRT. Observe that $(DASUB)$ can also be expressed in the object-level in Asher'
s
 logic of common-sense entailment. \par

        Now, we treat these cases in turn. The first produces $K_{1} + K_{2} +
 K_{3}$ as the following by $(DASUB)$: \par
\ \ \ $\langle \lbrace x, y, z, u \rbrace, \lbrace professor(x), 
phd\_student(y), supervize(x, y)$, \par
        $fail(z), \neg study(u), z = y = u \rbrace \rangle: \tau_{0}, z \sim y
 \sim u$ \par\noindent
The interpretation changes the label for accessibility. From this DRS, we can 
conclude by $(+E)$ that the Ph.D. student stopped to study the subject. \par
        On the other hand, the second yields the next DRS: \par
\ \ \ $\langle \lbrace x, y, z, u \rbrace, \lbrace professor(x), 
phd\_student(y), supervize(x, y)$, \par
        $fail(z), \neg study(u), z = y, u = x \rbrace \rangle: \tau_{0}, z 
\sim y, u \sim x$ \par\noindent
Then, we can infer that the professor stopped to study. \par
        But, assume that the following setence is added to the discourse: \par
\ \ \ But, he decided to rework a dissertation. \par\noindent
whose DRS $K_{4}$ is expressed as: \par\noindent
$K_{4}$: $\langle \lbrace w \rbrace, \lbrace rework(w), w = ? \rbrace \rangle$
 \par\noindent
By $(+I)$, we have the following for the first case: \par
$K_{1} + K_{2} + K_{3} + K_{4}$: $\langle \lbrace x, y, z, u \rbrace, \lbrace 
professor(x), phd\_student(y),$ \par
        supervize(x, y)$, fail(z), \neg study(u), u = z = y, rework(w), w = ? 
\rbrace \rangle: \tau_{0}, z \sim y \sim u$ \par\noindent
Since it is consistent to assume the student decided to rework, $(DASUB)$ can 
fill the incomplete condition, namely \par
\ \ \ $\langle \lbrace x, y, z, u, w \rbrace, \lbrace professor(x), 
phd\_student(y), supervize(x, y)$, \par
        $fail(z), \neg study(u), rework(w), u = z = y = w \rbrace \rangle: 
\tau_{0}, y \sim z \sim u \sim w$ \par\noindent
However, the second case is problematic. Applying $(+I)$ gives: \par
\ \ \ $\langle \lbrace x, y, z, u, w \rbrace, \lbrace professor(x), 
phd\_student(y), supervize(x, y)$, \par
        $fail(z), \neg study(u), u = x, z = y, rework(w), w = ? \rbrace 
\rangle: \tau_{0}, z \sim y, u \sim x$ \par\noindent
Obviously, to obtain the complete condition $w = u = x$ is blocked by $(DASUB)
$ because the fact the professor rewoked a dissertation induces inconsistency 
under the context of this discourse. As a consequence, the provious conclusion
 that the professor stopped to study the subject is also withdrawn. \par

        Although non-monotonic reasoning in discourse is subtle and complex, 
the proposed LDS formulation can cope with non-monotonicity in anaphora 
resolution without any difficulty. Together with a computational advantage of 
LDS, $LND$ can be used to model reasoning with DRSs. 
\par\noindent
\bf{Example 4}\rm\par\noindent
If he finds a donkey, John will beat it. \par
        This example is about cataphoric pronouns. By the DRS construction 
procedure, we obtain: \par
\ \ \ $\langle \lbrace \ \rbrace, \langle \lbrace x, y \rbrace, \lbrace x = ?,
 donkey(y), find(x, y) \rbrace \rangle$ \par
\ \ \ \ \ \ \ \ \ \ \ $\Rightarrow \langle \lbrace z, u \rbrace, \lbrace 
John(z), beat(z, u), u = ? \rbrace \rangle: \tau_{0}, x \sim z \sim u, y \sim 
z 
\sim u$ \par\noindent
Here, ``he" is a cataphoric pronoun coreferential with ``John". But it cannot 
be processed until the consequent DRS is introduced to supply enough 
information. When the construction finishes, the information about accesibilit
y 
is available. Unfortunately, accessibility  does not tell us a crue for anapho
ra 
resolution here. The intuitive account is that firstly we identify $u$ with $y
$ 
and $x$ with $z$. Other possibilities are non-monotonically rejected by 
$(DASUB)$. In this context, the bottom up construction based on the LDS 
formulation is suited to the incremental processing of anaphora resolution. 
\par

\bigskip


\noindent{\bf 4. Conclusions}\rm\par
\noindent
We propose a labelled deduction system to serve as an inference method for DRT
 based on Gabbay's LDS. To extract appropriate conclusions from a discourse 
under incomplete information, it is necessary to give a proof theory for 
manipulating a DRS as an information structure. In particular, we have emphasi
zed 
non-monotonic features of reasoning about DRSs. We believe that our approach w
ill
 be tenable if we focus on \it{intentional }\rm DRT (cf. Asher (1993)) to 
consider propositional attitudes in discourse. It seems also useful to the 
event-based description of discourse; see Kamp and Ryle (1993). \par

        Finally, we compare our system with related ones. Saurer (1993) 
proposed a natural deduction system for DRT based on Fitch-style formulation. 
In 
this sense, it seems difficult to implement it. In addition, Saurer's system 
assumes the top down construction procedure of Kamp and Ryle (1993). Reyle and
 
Gabbay (1994) developed a sequent-based proof system for DRT in which DRSs can
 be
 manipulated intuitionistically. Although their system offers an efficient 
algorithmic proof method for DRT, there may be some obstacles with a link to 
bottom up construction. Kamp and Ryle (1993) proposed the translation of DRT 
into first-order logic. This means that we can use a theorem-proving for 
first-order logic. But this may prevent us from extracting some important 
information in discourse. \par

\bigskip

\noindent{\bf References}\rm\par
\noindent
Akama, S. and Kobayashi, M. (1995): A labelled deductive approach to DRT I, 
\it{Proc. of the 5th International Workshop on Natural Language Understanding 
and Logic Programming, }\rm 23-37, Lisbon, Portugal. \par\noindent
Akama, S. and Nakayama, Y. (1994): Consequence relations in DRT, \it{Proc. of 
COLING-94, }\rm 1114-1117, Kyoto, Japan. \par\noindent
Akama, S. and Nakayama, Y. (1995): A three-valued semantics for Discourse
Representations, \it{Proc. of the IEEE 25th International Symposium on 
Multiple-Valued Logic, }\rm 123-128, Bloomington, USA. \par\noindent
Asher, N. (1991): Discourse Representation Theory and belief dynamics, A. 
Fuhrmann and M. Morreau (eds.), \it{The Logic of Theory Change, }\rm 282-321, 
Springer, Berlin. \par\noindent
Asher, N. (1993): \it{Reference to Abstract Objects in Discourse}\rm, Kluwer, 
Dordrecht. \par\noindent
Gabbay, D. (1993): Labelled deductive systems and situation theory, P. Aczel, 
D. Israel, Y. Katagiri, and S. Peters (eds.), \it{Situation Theory and its 
Applications vol. 3, }\rm 89-117, CSLI Lecture Notes, Stanford. \par\noindent
Gabbay, D. (1996): \it{Labelled Deductive Systems, }\rm Oxford University 
Press, Oxford, to appear. \par\noindent
Kamp, H. and Reyle, U. (1993): \it{From Discourse to Logic: Introduction to 
Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse 
Representation Theory, }\rm Two Parts, Kluwer, Dordrecht. \par\noindent
Prawitz, D. (1965): \it{Natural Deduction: A Proof-Theoretical Study, }\rm 
Almqvist and Wiksell, Stockholm. \par\noindent
Reyle, U. and Gabbay, D. (1994): Direct deductive computation on discourse 
representation structures, \it{Linguistics and Philosophy 17, }\rm 343-390. 
\par\noindent
Saurer, W. (1993): A natural deduction system for discourse representation the
ory, \it{The Journal of Philosophical Logic 22, }\rm 249-302.  \par\noindent

\end{document}
