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.
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 [
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 [
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 dificult 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 (A), together with the one of (B), implies the logical representation of (C). That is: the following formula should be derivable.
() () () (1) ⏞∃1¬sm⏟ile(1) ∧ ⏞A has-he⏟adache() ⇒ ⏞∃(¬smile() ∧ h⏟as-headache()) 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) ⏞¬(∀1sm⏟ile(1)) ∧ ⏞A has-he⏟adache() ⇒ ⏞∃(¬smile() ∧ h⏟as-headache()) Remark that we represent the pronoun “he” by a variable bound by an occurrence of the quantifier A .
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 the usual connectives and quantifiers of ifrst order logic ¬, ⇒, ∧, ∨, ∀, ∃ , and the anaphoric quantifier A . That is: we add the following formation rule to the usual ones of multisorted first-order logic: if is a formula and s is a variable of atomic sort , then A s is a formula (in which any occurrence of s is bound).
A sequent Γ ⊢ Δ, is an expression where Γ and Δ are finite (possibly empty) multisets of formulae. We use Greek capital letters Γ, Δ, Π, Σ, . . . 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. 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 ∃L and ∀R, s does not appear in Γ, Δ. The number of premises of A L is at least one. In A R, the constant 1s, . . . , s are all and only the constants of sort s appearing in Γ.
The first condition is the usual condition on quantifiers in first-order logic. For the A R, we require that the constants s does appear, but they must appear in Γ on the left-hand side of the turnstile. For the 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 Γ ⊢ Δ if k appears in some formula in Γ. Let D be a prederivation, and = 0, . . . , a path in D where 0 is the root of D and is the mother of +1 for all < . We say a constant k appears negatively in if k appears negatively in one of the path’s sequents.
Definition 2. A prederivation is a derivation if, whenever Γ1, (k1), . . . , Γ, (k) are the premises of an L rule then 1s, . . . ks are all and only the constants of sort s which appear negatively in the path from the root of the derivation D to the conclusion Γ1, . . . , Γ, ⊢ Δ1, . . . Δ of the rule.
Notation we use 1, 2, 3, . . . for variables that are bounded by a universal or an existential quantifier and 1, 2, 3 . . . for variables that are bounded by an anaphoric quantifier.
Bathroom sentence Consider the sentence “Either there is no bathroom in this house or it is upstairs”. Clearly the pronoun “it” refers to “the bathroom” i.e., we expect that 3 below entails 4. (3) (¬∃1Bathroom(1)) ∨ A 1Upstairs(1) (4) (¬∃1Bathroom(1)) ∨ (∃2(Bathroom(2) ∧ Upstairs(2))
The proof below shows how we derive the entailment 3 ⊢ 4. The condition on the A L rule is satisfied trivially, since 1 appears directly in the conclusion of the rule (in the formula coloured blue) and 1 is the only constant which appears in the path from the conclusion of the rule to the root of the proof.
Ax (k1) ⊢ (k1) (k1) ⊢ (k1)
(k1), (k1) ⊢ ((k1) ∧ (k1)) (k1), (k1) ⊢ ∃2((2) ∧ (2)) ∃ ¬∃¬1∃(11)(⊢1¬))∃∨1A (11)(A),x∃1A(A11)1⊢(¬(1∃)1,)∃1,1((k1(1)),1∃⊢)⊢∃2(∃2((2((2)(2∧)2∧) (∧(2)()2)2)))RA∃∨LLL ¬∃1(1)) ∨ A 1U(), ∃1(1) ⊢ ¬∃1(1), ∃2((2) ∧ (2)) ¬ R ¬∃1¬(∃11))∨(A1))1∨ A()1⊢¬(∃)⊢1¬(∃11),¬(∃11),∃(21(),∃(22)(∧(2()2∧)) (2))R C⇒R (¬∃1(1)) ∨ A 1 () ⊢ (¬∃1(1)) ∨ (∃2((2) ∧ (2))) ∨ Ax ∧R R Donkey sentences Consider the sentence “If a monster fights Guts then he kills it”. Here the pronoun “he” refers to Guts since Guts is an (imaginary) human being while the pronoun “it” refer to “a monster”. Moreover, the pronoun “it” has a universal reading: what the sentence means is “Any monster that fights Guts will be killed by Guts”. Thus we expect that 5 below implies 6.
(5) [∃1ℎ(Monster(1) ∧ Fight(g, 1))] ⇒ A 1A ℎKill(1, 2) 2 (6) ∀2ℎ[Monster(2) ∧ Fight(g, 2) ⇒ Kill(g, 2)]
The proof below shows how we derive the entailment 5 ⊢ 6. The condition on the first A L-rule (the one colored in red) is satisfied trivially, since is the only constant of sort (male human) which appears in the path from the conclusion to the root. The condition on the other A L is also trivially satisfied: k1ℎ is the only constant of sort ℎ (non-human) appearing in the path proof.
(k1) ∧ (g, k1) ⊢ (k1) ∧ (g, k1)
Ax (k1) ∧ (g, k1) ⊢ ∃1ℎ( (1) ∧ (g, 1)) [∃1ℎ( (1) ∧ (g, 1))] ⇒ A 1A 2(1, 2) ⊢ ∀2[ (2) ∧ (g, 2) ⇒ (g, 2)] ∀ (g, k1) ⊢ (g, k1)
Ax A 2ℎ(g, 2) ⊢ (g, k1)
A L
The reader can check that the formula in 1 is derivable, while there is no derivation of the formula in 2
Let the expression A {1,...,}.[] (A is indexed by a finite set of constants) stand for the classical formula [1] ∨ · · · ∨ []. The A rules of SAC, adding the proper indices, become derivable as particular cases of ∨ 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 A .[] instead of the disjunction ∨∈ [] 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 A .[]: there is a finite set of constants = {1, . . . , } such that the formula [1] ∨ · · · ∨ [] is true. This establishes the soundness of SAC.
We have introduced SAC, a sequent calculus for anaphora resolution, which corresponds to
the resolution with argumentative dialogues of [