# A proof system for dialogical anaphora resolution

Davide Catta, Richard Moot, Christian Retoré, Symon Jory Stevens-Guille

## ► To cite this version:

Davide Catta, Richard Moot, Christian Retoré, Symon Jory Stevens-Guille. A proof system for dialogical anaphora resolution. AI3 2022 - 5th Workshop on Advances in Argumentation in Artificial Intelligence, Nov 2022, Udine, Italy. lirmm-03863462

HAL Id: lirmm-03863462

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03863462

Submitted on 21 Nov 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# A Proof System for Dialogical Anaphora Resolution

Davide Catta¹, Richard Moot², Christian Retoré² and Symon Steven-Guille³

¹Télécom Paris / CNRS LTCI - UMR5141

²CNRS, LIRMM, Univ Montpellier

³Ohio State University

**Abstract**

We present a proof-theoretic account of anaphora resolution, namely a sequent calculus corresponding to dialogical games where two players argue to find the reference of some anaphor.

**Keywords**

logic, proof theory, formal semantics, anaphora resolution, dialogical games

## 1. Introduction

In our ongoing work, we propose a proof-theoretic account of anaphora resolution, focusing on pronominal reference to entities. Our account is motivated by the view that knowledge of possible anaphoric dependencies in natural language should be considered part of semantic competence rather than merely the byproduct of extralinguistic mechanisms. Consequently, our account uses the standard tools of contemporary semantic theory, namely formal logic, to model possible resolutions of anaphoric expressions. Unlike most previous work in this tradition [1, 2], we resolve anaphora in the proof theory of our logic, not by checking the model-theoretic truth of some oracle's chosen indexing or reuse of variables. In [3] two of the authors of the present work introduced a dialogical argumentation framework for solving anaphoric dependencies in sentences. This framework introduced a new quantifier (the anaphoric quantifier $\mathcal{A}$) whose formal meaning is defined by the way in which a formula having $\mathcal{A}$ as main connective can be attacked and defended in a dialogical logic [4, 5] inspired framework. Here we present a sequent calculus formalism in which the two rules for the quantifier $\mathcal{A}$ precisely capture those of the above-mentioned dialogical system above.

In Section 2 we introduce the linguistic phenomenon to be modelled — anaphoric reference to entities by pronouns. Section 3 introduces the sequent calculus whose rules implicitly define the meaning of our new quantifier. Section 4 illustrates applications of the logic with commented proofs of the expected readings of pronouns. In particular, we give examples of specific patterns of reference which have attracted the attention of linguists and logicians in the literature: donkey sentences [6] and bathroom sentences.¹ Section 5 briefly discusses soundness for our logic, and Section 6 concludes.

Advances In Argumentation In Artificial Intelligence AI³, November 28-December 2, 2022

<figure><img src="image_2.png" /></figure>

© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

<figure><img src="image_3.png" /></figure>

CEUR Workshop Proceedings (CEUR-WS.org)

¹Roberts [7] attributes the bathroom sentence to Barbara Partee while noting a similar example in [8]
## 2. Anaphora, pronouns and inferences

Anaphora is the linguistic phenomenon whereby the interpretation of one occurrence of an expression depends on the interpretation of an occurrence of another expression. This characterisation allows us to recognise that in the two sentences “Gertrude eats an apple. It is delicious” the pronoun “it” is anaphoric. The interpretation of the pronoun “it” is the same as the interpretation of the noun “an apple”. Let us call the linguistic expression on which the interpretation of an anaphor depends the antecedent. Humans are generally able to resolve anaphora correctly, i.e., find an appropriate antecedent for an anaphoric expression. Anaphora resolution is a difficult task in natural language processing. We consider anaphora resolution to be an inferential problem. If, for example, the assertion of the two sentences “(A) someone does not smile” and “(B) he has a headache” is justified, then we can conclude that the sentence “(C) someone has a headache and does not smile” is justified. On the contrary, if the assertion of the two sentences “(D) not everyone smiled” and “(B) he had a headache” is justified, then we cannot conclude that the assertion of the sentence “‘(C) someone has a headache and does not smile” is justified. In our framework, this will be represented by the fact that the logical representation of (1), together with the one of (2), implies the logical representation of (3). That is: the following formula should be derivable.

$$ (1) \quad \overbrace{\exists x_1 \neg \text{smile}(x_1)}^{(A)} \wedge \overbrace{\mathcal{A} y \text{ has-headache}(y)}^{(B)} \Rightarrow \overbrace{\exists z (\neg \text{smile}(z) \wedge \text{has-headache}(z))}^{(C)} $$

On the contrary, the representation of (D) together with the one of (B) does not imply the logical representation of (C). Thus, the following formula should not be derivable

$$ (2) \quad \overbrace{\neg(\forall x_1 \text{smile}(x_1))}^{(D)} \wedge \overbrace{\mathcal{A} y \text{ has-headache}(y)}^{(B)} \Rightarrow \overbrace{\exists z (\neg \text{smile}(z) \wedge \text{has-headache}(z))}^{(C)} $$

Remark that we represent the pronoun “he” by a variable bound by an occurrence of the quantifier $\mathcal{A}$.

## 3. The sequent calculus SAC

We consider a standard first order multisorted language (the reader can consult [9, Chapter 3] for definitions) in which the set of sorted terms only contains variables and constants. Formulae are generated from a set of atomic formulae using the usual connectives and quantifiers of first order logic $\neg, \Rightarrow, \land, \lor, \forall, \exists$, and the anaphoric quantifier $\mathcal{A}$. That is: we add the following formation rule to the usual ones of multisorted first-order logic: if $\mathcal{A}$ is a formula and $x^s$ is a variable of atomic sort $s$, then $\mathcal{A} x^s \mathcal{A}$ is a formula (in which any occurrence of $x^s$ is bound).

A sequent $\Gamma \vdash \Delta$, is an expression where $\Gamma$ and $\Delta$ are finite (possibly empty) multisets of formulae. We use Greek capital letters $\Gamma, \Delta, \Pi, \Sigma, \dots$ to denote arbitrary multisets of formulas.

A sequent calculus is a formalism to construct formal deductive arguments. The arguments, called derivations or proofs, are obtained through the application of inference rules. Inference rules have a (possibly empty) list of sequents as premise and a sequent as conclusion. Proofs in the sequent calculus are trees of sequents that are constructed from a given set of rules.
<figure><img src="image_4.png" /><figcaption>**Table 1**
The sequent calculus SAC</figcaption></figure>

**Definition 1.** Given the rules in Table 1, a prederivation in SAC (Sequent Anaphoric Calculus) is a tree where each local subtree is an instance of one of the rules subject to the following conditions: in the premises of $\exists^L$ and $\forall^R$, $k^s$ does not appear in $\Gamma$, $\Delta$. The number of premises of $\mathcal{A}^L$ is at least one. In $\mathcal{A}^R$, the constant $k_1^{s_1}, \dots, k_n^{s_n}$ are all and only the constants of sort s appearing in $\Gamma$.

The first condition is the usual condition on quantifiers in first-order logic. For the $\mathcal{A}^R$, we require that the constants $k_i^s$ does appear, but they must appear in $\Gamma$ on the left-hand side of the turnstile. For the $\mathcal{A}^L$ we require for the moment only that the rule has at least one premise, but we will refine this when moving from prederivations to derivations.

We say that a constant k appears negatively in a sequent $\Gamma \vdash \Delta$ if k appears in some formula in $\Gamma$. Let $\mathcal{D}$ be a prederivation, and $\mathcal{P} = x_0, \dots, x_n$ a path in $\mathcal{D}$ where $x_0$ is the root of $\mathcal{D}$ and $x_i$ is the mother of $x_{i+1}$ for all $i < n$. We say a constant $k^s$ appears negatively in $\mathcal{P}$ if $k_s$ appears negatively in one of the path's sequents.

**Definition 2.** A prederivation is a derivation if, whenever $\Gamma_1, B(k_1^s), \dots, \Gamma_n, B(k_n^s)$ are the $n$ premises of an $\mathcal{A}^L$ rule then $k_1^s, \dots, k_n^s$ are all and only the constants of sort s which appear negatively in the path from the root of the derivation $\mathcal{D}$ to the conclusion $\Gamma_1, \dots, \Gamma_n, A^s B \vdash \Delta_1, \dots, \Delta_n$ of the rule.

**Notation** we use $x_1, x_2, x_3, \dots$ for variables that are bounded by a universal or an existential quantifier and $y_1, y_2, y_3, \dots$ for variables that are bounded by an anaphoric quantifier.
The reader can check that the formula in 1 is derivable, while there is no derivation of the formula in 2

5. Relation to LK and soundness

Let the expression $\mathcal{A}\{k_1^s, ..., k_p^s\}x.A[x]$ ($\mathcal{A}$ is indexed by a finite set of constants) stand for the classical formula $A[k_1^s] \vee \dots \vee A[k_p^s]$. The $\mathcal{A}$ rules of SAC, adding the proper indices, become derivable as particular cases of $\vee$ rules. Our calculus SAC consists of a proper subset of classical proofs in LK sequent calculus (more precisely LK without the rules of weakening) with $\mathcal{A}^K.A[x]$ instead of the disjunction $\vee_{k \in K} A[k]^2$ in which all superscripts are thereafter masked: a proof in SAC is the projection of a proof in LK. Because provable sequents in LK are true in all models, so are ours with the meaning of $\mathcal{A}x.A[x]$: there is a finite set of constants $K = \{k_1^s, ..., k_p^s\}$ such that the formula $A[k_1^s] \vee \dots \vee A[k_p^s]$ is true. This establishes the soundness of SAC.

6. Conclusions and future work

We have introduced SAC, a sequent calculus for anaphora resolution, which corresponds to the resolution with argumentative dialogues of [3]. We illustrated how it can be use to solve several standard puzzles concerning anaphoric dependencies in formal semantics. In the future, as SAC enjoys soundness (cf. previous section), we intend to establish completeness by defining a model as a family of relevant logic models in order to express the global conditions on proofs.

References

[1] H. Kamp, A theory of truth and semantic representation, in: Truth, interpretation and information, Foris Dordrecht, 1984, pp. 1–41.

[2] J. Groenendijk, M. Stokhof, Dynamic predicate logic, Linguist Philos (1991) 39–100.

[3] D. Catta, S. Stevens-Guille, Lorenzen won the game, Lorenz did too: Dialogical logic for anaphora and ellipsis resolution, in: A. Silva, R. Wasserman, R. de Queiroz (Eds.), WoLLIC 2021, volume 13038 of LNCS, Springer, 2021.

[4] P. Lorenzen, Logik und agon, Atti Del XII Congresso Int. di Filosofia 4 (1958) 187–194.

[5] P. Lorenzen, K. Lorenz, Dialogische Logik, Wissenschaftliche Buchgesellschaft, 1978.

[6] P. T. Geach, Reference and generality: An examination of some medieval and modern theories, Mind 73 (1964) 575–583.

[7] C. Roberts, Modal subordination and pronominal anaphora in discourse, Linguist Philos 12 (1989) 683–721.

[8] G. Evans, Pronouns, quantifiers, and relative clauses (I), Can. J. Philos 7 (1977) 467–536.

[9] R. Moot, C. Retoré, The logic of categorial grammars: a deductive account of natural language syntax and semantics, volume 6850 of LNCS, Springer, 2012.

<footnote n="2">²From the rules of classical logic one clearly has $\mathcal{A}^K x.A[x] \vdash \mathcal{A}^{K \cup J} x.A[x]$.</footnote>