\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}