The Challenge of Composition inDistributional and Formal Semantics
Part II
Ran Tian1 , Koji Mineshima2 and Pascual Martı́nez-Gómez3
1 Tohoku University, Japan

2 Ochanomizu University, Japan
3 AIST, JapanIJCNLP 2017, Taipei, Taiwan
November 27, 2017
1 / 51

Three Challenges
1. Meaning Representations (MRs): what are proper MRs for natural
languages?
2. Compositional Semantics: how to compute the MR of a complex
expression from the MRs of its parts?
3. Inference: how can we do inference with MRs?
• We start with Question 2:• Combinatory Categorial Grammar (CCG)• Lambda Calculus• And then move on to Question 1 and Question 3• Predicate-argument structure, first-order logic, andhigher-order Logic• Inference-first conception: an MR is good if it enables correctand efficient inferences

2 / 51

Semantic Composition via Phrase Structure Grammar
S

→

NP VP

NP

→

Det N

VP

→

TV NP

Det
N
NP
TV

→
→
→
→

the
diplomatTaipei
left

S

VP

NP

Det
The

N
diplomat

TV
left

NP
Taipei3 / 51

Semantic Composition via Phrase Structure Grammar
S

→

NP VP

NP

→

Det N

VP

→

TV NP

Det
N
NP
TV

→
→
→
→

the
diplomatTaipei
left

S

VP

NP

Det
The
M1

N
diplomat
M2

TV
left
M3

NP
Taipei
M4• Assign a MR to each leaf node

3 / 51

Semantic Composition via Phrase Structure Grammar
S

→

NP VP

NP → Det N[[NP]] = [[Det]] ⊕2 [[N]]NP
VP → TV NP
M1 ⊕2 M2[[VP]] = [[TV ]] ⊕3 [[NP]]Det → theN → diplomat
N
Det
NP → Taipei
diplomat
The
TV → left
M2
M1

S

VP
M3 ⊕ 3 M4
TV
left
M3

NP
Taipei
M4• Assign a MR to each leaf node

• Compute the MR of each phrase in terms of the MRs of its parts,

according to meaning composition rules

3 / 51

Semantic Composition via Phrase Structure Grammar
S
S → NP VP(M1 ⊕1 M2 ) ⊕1 (M3 ⊕2 M4 )[[S]] = [[NP]] ⊕1 [[VP]]
NP → Det N[[NP]] = [[Det]] ⊕2 [[N]]
VP
NP
VP → TV NP
M3 ⊕ 3 M4
M1 ⊕2 M2[[VP]] = [[TV ]] ⊕3 [[NP]]Det → theN → diplomat
NP
TV
N
Det
NP → Taipei
Taipeileft
diplomat
The
TV → left
M2
M1
M4
M3
• Assign a MR to each leaf node

• Compute the MR of each phrase in terms of the MRs of its parts,

according to meaning composition rules

3 / 51

Semantic Composition via Phrase Structure Grammar
S
S → NP VP(M1 ⊕1 M2 ) ⊕1 (M3 ⊕2 M4 )[[S]] = [[NP]] ⊕1 [[VP]]
NP → Det N[[NP]] = [[Det]] ⊕2 [[N]]
VP
NP
VP → TV NP
M3 ⊕ 3 M4
M1 ⊕2 M2[[VP]] = [[TV ]] ⊕3 [[NP]]Det → theN → diplomat
NP
TV
N
Det
NP → Taipei
Taipeileft
diplomat
The
TV → left
M2
M1
M4
M3
• Assign a MR to each leaf node

• Compute the MR of each phrase in terms of the MRs of its parts,

according to meaning composition rules• Many grammar rules, many composition rules
3 / 51

Semantic Composition via Categorial Grammar (CG)
S

NP

Det
The

VP

N
diplomat

TV
left

NP
Taipei4 / 51

Semantic Composition via Categorial Grammar (CG)
S

NP

Det
The

S\NP

N
diplomat

TV
left

NP
Taipei4 / 51

Semantic Composition via Categorial Grammar (CG)
S

NP

NP/N
The

S\NP

N
diplomat(S\NP)/NP
left

NP
Taipei4 / 51

Semantic Composition via Categorial Grammar (CG)
S

NP

NP/N
The

S\NP

N
diplomat(S\NP)/NP
left

NP
Taipei• A small set of basic categories (S, NP, N)• Each functional category of the form X /Y and X \Y specifies how

words combine with each other.
4 / 51

Semantic Composition via Categorial Grammar (CG)
S

NP

NP/N
The
λF .ιx.F (x)S\NPN
diplomatλx.diplomat(x)(S\NP)/NPleft
λy λx.left(x, y)NP
TaipeiTaipei• A small set of basic categories (S, NP, N)• Each functional category of the form X /Y and X \Y specifies how

words combine with each other and, at the same time, how tocompute the MR of a phrase node.

4 / 51

Semantic Composition via Categorial Grammar (CG)SNP
ιx.diplomat(x)NP/NThe
λF .ιx.F (x)Ndiplomatλx.diplomat(x)S\NPλx.left(x, Taipei)(S\NP)/NPleft
λy λx.left(x, y)NP
TaipeiTaipei• A small set of basic categories (S, NP, N)• Each functional category of the form X /Y and X \Y specifies how

words combine with each other and, at the same time, how tocompute the MR of a phrase node.

4 / 51

Semantic Composition via Categorial Grammar (CG)S
left(ιx.diplomat(x), Taipei)
NPιx.diplomat(x)NP/NThe
λF .ιx.F (x)Ndiplomatλx.diplomat(x)S\NPλx.left(x, Taipei)(S\NP)/NPleft
λy λx.left(x, y)NP
TaipeiTaipei• A small set of basic categories (S, NP, N)• Each functional category of the form X /Y and X \Y specifies how

words combine with each other and, at the same time, how tocompute the MR of a phrase node.
• A small set of grammar rules and meaning composition rules

4 / 51

Combinatory Rules
Forward Function Application
X
F (M)
X/Y
F

Y
M

Backward Function Application
X
F (M)
Y
M

X\Y
F
5 / 51

Derivation trees• Turn the tree upside down (for a historical reason)• Derivation trees (proof trees)

likes(S\NP)/NPλyλx.like(x, y)

John
NP
john

Mary
NP
mary
>

S\NP
λx.like(x, mary )<Slike(john, mary )• Function Application rules

X /Y
F

X
F (M)

Y
M

Y
M
>

X \Y
F
X
F (M)

<

6 / 51

From AB to CCG• The fragment of categorial grammar consisting of function

application rules is called AB grammar (Ajdukiewicz, 1935;
Bar-Hillel, 1953)• Adding more combinatory rules leads to Combinatory Categorial

Grammar (CCG) (Steedman, 2000, 2012)

7 / 51More combinatory rules
Function Composition rules
X /Y
f

Y /Z
g

X /Z
λx.f (g(x))

>B

Y \Z
g

X \Y
f

X \Z
λx.f (g(x))<B

Crossed Composition rules
X /Y
f

Y \Z
g

X \Z
λx.f (g(x))

> B×

Y /Z
g

X \Y
f

X /Z
λx.f (g(x))< B×

8 / 51

A more complicated derivation
John doesn’t like Mary
¬like(john, mary )doesn’t(S\NP)/ (S\NP)λF λx.¬F (x)
John
NP
john

like
(S\NP) /NP
λy λx.like(x, y )(S\NP)/NPλy λx.¬like(x, y )S\NPλx.¬like(x, mary )S¬like(john, mary )

Mary
NP
mary

>B

>

<

Right node raising shows that doesn’t like can be a constituent:
John [[respects] but [doesn’t like]] Mary.
respect(john, mary ) ∧ ¬like(john, mary )9 / 51

Lambda Calculus• A formal system to represent computation• Simple yet very expressivefunctionλx.x + 2
λx.walk(x)inputnumber x
entity x

outputx +2
proposition walk(x)β-conversion (simplification, substitution):functionargument(λx. [. . . x . . .]) (a) = [ . . . a . . . ]Examples:• (λx.x + 2)(5) = 5 + 2• (λx.walk(x))(john) = walk(john)
10 / 51

β-conversion: more examples
β-conversion (simplification):functionargument(λx. [. . . x . . .]) (a) = [ . . . a . . . ]1. ( λx.like(x, y ) )( john ) = like(john, y)
2. ( λy .like(x, y ) )( john ) = like(x, john)
3. ( λx.like(x, x) )( john ) = like(john, john)
4. ( λx.like(mary , x) ∧ boy(x) )( john ) = like(mary, john) ∧ boy (john)
5. (( λy .λx.like(x, y ) )( john ))(mary ) =( λx.like(x, john) )( mary ) = like(mary, john)
11 / 51α-conversion
α-conversion (renaming):
λ x .[ . . . x . . . ] = λ y .[ . . . y . . . ]12 / 51α-conversion
α-conversion (renaming):
λ x .[ . . . x . . . ] = λ y .[ . . . y . . . ]Example:λx.boy (x) ∧ love(x)(z) =✻✻λy .boy (y ) ∧ love(y)(z)✻✻

12 / 51α-conversion
α-conversion (renaming):
λ x .[ . . . x . . . ] = λ y .[ . . . y . . . ]Example:λx.boy (x) ∧ love(x)(z) =✻✻λy .boy (y ) ∧ love(y)(z)✻✻Lambda calculus vs. Set Theory
Lambda calculus
λx.Fx(λx.Fx)(a)(λx.Fx)(a) = Fa

Set Theory{x | Fx}a ∈ {x | Fx}a ∈ {x | Fx} ⇔ Fa

12 / 51

Adding type information• But is meaning composition via lambda calculus always safe?
• What we need: Type safety• Type safety lies at the heart of formal compositional semantics

13 / 51

Adding type information• But is meaning composition via lambda calculus always safe?
• What we need: Type safety• Type safety lies at the heart of formal compositional semantics

Define simple types:

Examples:john, mary :λx.walk(x) :λy.λx.like(x, y) :

Type
E
T
X →Y

Meaning
EntityProposition
A function from X to Y

E
E→T
E → (E → T)

entityfunction from entities
to propositions
function from two entities
to propositions

13 / 51

Adding type information• But is meaning composition via lambda calculus always safe?
• What we need: Type safety• Type safety lies at the heart of formal compositional semantics

Define simple types:

Examples:john, mary :λx.walk(x) :λy.λx.like(x, y) :walk(john) :

Type
E
T
X →Y

Meaning
EntityProposition
A function from X to Y

E
E→T
E → (E → T)T

entityfunction from entities
to propositions
function from two entities
to propositions
proposition
13 / 51

Adding type information• But is meaning composition via lambda calculus always safe?
• What we need: Type safety• Type safety lies at the heart of formal compositional semantics

Define simple types:

Examples:john, mary :λx.walk(x) :

Type
E
T
X →Y

Meaning
EntityProposition
A function from X to YEE→T

λy.λx.like(x, y) :E → (E → T)walk(john) :like(john, mary ) :TTentityfunction from entities
to propositions
function from two entities
to propositions
proposition
proposition
13 / 51

Adding type information• But is meaning composition via lambda calculus always safe?
• What we need: Type safety• Type safety lies at the heart of formal compositional semantics

Define simple types:

Examples:john, mary :λx.walk(x) :

Type
E
T
X →Y

Meaning
EntityProposition
A function from X to YEE→T

λy.λx.like(x, y) :E → (E → T)walk(john) :like(john, mary ) :walk(like) :TT# type-mismatch

entityfunction from entities
to propositions
function from two entities
to propositions
proposition
proposition
13 / 51

Types control semantic composition
β-conversion (simplification):
Type: A → B

Type: A

Type: B

(λx. [. . . x . . .]) (a) = [ . . . a . . . ]14 / 51

Types control semantic composition
β-conversion (simplification):
Type: A → B

Type: A

Type: B

(λx. [. . . x . . .]) (a) = [ . . . a . . . ]Example:Type: E → T(λx.walk(x)Type: T

Type: E(john)=

walk(john)

14 / 51

CCG-based Compositional Semantics• Type information is always implicit in CCG-derivation trees

likes(S\NP)/NP
λy.λx.like(x, y)
John
NP
john

Mary
NP
mary

>

S\NP
λx.like(x, mary )Slike(john, mary )<15 / 51

CCG-based Compositional Semantics• Type information is always implicit in CCG-derivation trees

likes(S\NP)/NP
λy.λx.like(x, y) : E → (E → T)John
NPjohn : E

MaryNPmary : E>

S\NP
λx.like(x, mary ) : E → T

S
like(john, mary ) : T<

15 / 51

Syntactic sugar

Special symbols (constants) to represent logical expression:
Logical expression
¬
∧
∨
→
∀
∃
ι

Type
T→T
T → (T → T)
T → (T → T)
T → (T → T)
(E → T) → T(E → T) → T(E → T) → E

negationconjunction
disjunction
implication
universal quantifier
existential quantifier
iota operator

We can write :and so on.

A∧B
∀xFx
∃xFx

for
for
for

∧(A, B)∀(λx.Fx)∃(λx.Fx)• Logics can be encoded in Lambda Calculus!

16 / 51

From categories to types
Define a homomorphism (·)• from categories to types:
NP • = E
S• = T(Y /X )• = (Y \X )• = X • → Y •Example:• (S\NP)• = E → T (intransitive verbs)• ((S\NP)/NP)• = E → (E → T) (transitive verbs)• As for as type homomorphism is preserved in the lexicon, there isno danger of type-clash during meaning composition.

17 / 51

Lexicon: open words and closed words• For an open word, we can use a template to specify its MR.
• ϕ is the position in which the lemma of a word appears.

Category
S\NP(S\NP)/NP

Meaning templates
λx.ϕ(x)λy .λx.ϕ(x, y )

Type
E→T
E → (E → T)

• For a closed word, we can directly assign its MR.

• For example, if we are interested in logical expressions, we canuse the following lexical entries:

Lemma
some
every
no

Category
NP/N
NP/N
NP/N

MR
λF λG.∃x(Fx ∧ Gx)
λF λG.∀x(Fx ∧ Gx)
λF λG.¬∃x(Fx ∧ Gx)

Type(E → T) → (E → T) → T(E → T) → (E → T) → T(E → T) → (E → T) → T
18 / 51

Excerpts of Templates from ccg2lambda
CCG category
NP
S\NPnom
S\NPnom /NPacc
S/S
NP/NP

Meaning Representation
λNF .∃x(N(ϕ, x) ∧ F (x))λQK .Q(λI.I, λx.∃v (K (ϕ, v ) ∧ (Nom (v ) = x)))λQ2 Q1 K .Q1 (λI.I, λx1 .Q2 (λI.I, λx2 .∃v (K (ϕ, v )∧ (Nom (v ) = x1 ) ∧ (Acc (v ) = x2 ))))
λSK .S(λJv .K (λv ′ .(J(v ′ ) ∧ ϕ(v ′ )), v ))λQNF .Q(λGx.N(λy .(ϕ(y) ∧ G(y )), x), F )Types
Type ::= E | Event | T | X ⇒ Y
Mapping from syntactic categories to semantic types
NP • = ((E → T) → E → T) → (E → T) → T
S • = ((Event → T) → Event → T) → T(C1/C2)• = (C1\C2)• = C2• → C1•
19 / 51

English!CCG!parser" !Penn!Treebank!
" !CCGBank!

(S (NP-SBJ-1 John)(VP (VBN met)
(NP Mary)))![Hockenmaier!and!Steedman!2007]!

S
NP" CCG!parser!

!W!C&C![Curran!and!Clark!2007]!
!W!EasyCCG![Lewis!and!Steedman!EMNLP2014]!
!W!depccg![Yoshikawa+!ACL2017]!

" Seman)c!Parser!

W!Boxer![Bos+!2004]!
W!Langpro![Abzianidze!EMNLP2015]!
W!ccg2lambda![Mineshima+!EMNLP2015]!
!

John

John
NP
j

S[pt]\NPS[pt]\NP/NP

NP

met

Mary

met
S[pt]\N P/N P
y x.(meet(x, y))S[pt]\N P
x.(meet(x, m))S[pt]meet(j, m)

Mary
NP
m
>

<

6

20 / 51

Japanese!CCG!parser" !Kyoto/NAIST!Corpus!
" !Japanese!CCGBank!

大使がambassadorACC

交渉に
negoatiationDAT![Uematsu+!ACL2013]!

" !CCG!parser!(Jigg,!depccg)!

!!!W!Jigg![Noji!and!Miyao!ACL2016]!
!!!W!depccg![Yoshikawa+!ACL2017]!

" Seman)c!parser!(ccg2lambda)!

参加した
participatePAST

VP

PP

VP

Noun

PostP

大使

が

PP

VP

Noun

PostP

交渉

に

VP

Aux

Noun

Verb

参加

し

た

!!W!ccg2lambda!![Mineshima+!EMNLP2016]!

21 / 51Three levels of MRs• (Level 0 : Individual words)• Level 1 : Predicate-Argument structure• Level 2 : Basic logical features (negation, disjunction, etc.)• Level 3 : Higher-order logical features

22 / 51

Level 1: Predicate-Argument Structure• Who did what, where, when?

• MRs in Event semantics (Parsons, 1990):

Brutus stabbed Caesar on the street at noon.
∃e(stab(e) ∧ (subj(e) = brutus) ∧ (obj(e) = caesar ) ∧(location(e) = street) ∧ (time(e) = noon))• MRs have a flat structure with:• ∃ (existential quantifier)• ∧ (conjunction)• Extensional descriptions of scenes or situations

23 / 51

Other notations: DRS and Graph• Discourse Representation Structure (DRS) (Kamp and Reyle, 1993):estab(e)subj(e) = brutus
obj(e) = caesar
location(e) = streettime(e) = noon

• Graph notation:

time

noon

subj
brutusstreet•stab

carsarobj

location• These three notations deliver the same information

24 / 51

The Diamond Inference(1) Brutus stabbed Caesar on the street at noon.
⇒ (2) Brutus stabbed Caesar on the street⇒ (3) Brutus stabbed Caesar at noon.
⇒ (4) Brutus stabbed Caesar.
(1)

(2)

(3)

(4)

e
stab(e)subj(e) = brutus
obj(e) = caesar
location(e) = streettime(e) = noon

25 / 51

The Diamond Inference(1) Brutus stabbed Caesar on the street at noon.
⇒ (2) Brutus stabbed Caesar on the street⇒ (3) Brutus stabbed Caesar at noon.
⇒ (4) Brutus stabbed Caesar.
(1)

(2)

(3)

(4)

e
stab(e)subj(e) = brutus
obj(e) = caesar
location(e) = streettime(e) = noon

25 / 51

The Diamond Inference(1) Brutus stabbed Caesar on the street at noon.
⇒ (2) Brutus stabbed Caesar on the street⇒ (3) Brutus stabbed Caesar at noon.
⇒ (4) Brutus stabbed Caesar.
(1)

(2)

(3)

(4)

e
stab(e)subj(e) = brutus
obj(e) = caesar
location(e) = streettime(e) = noon

25 / 51

The Diamond Inference(1) Brutus stabbed Caesar on the street at noon.
⇒ (2) Brutus stabbed Caesar on the street⇒ (3) Brutus stabbed Caesar at noon.
⇒ (4) Brutus stabbed Caesar.
(1)

(2)

(3)

(4)

e
stab(e)subj(e) = brutus
obj(e) = caesar
location(e) = streettime(e) = noon

25 / 51

The Semantics of Voice• Perceptual report:

John saw Bob walking on the street.
⇒ Bob walked on the street.
subj
Bob

street

subj
•walk

obj

•see

John

location• Active-Passive alternation:

Brutus stabbed Caesar.
⇒ Caesar was stabbed by Brutus.
• Causative-inchoative alternation:
John closed the door.
⇒ The door became closed.

26 / 51

Level 2: Basic logical features• Add basic logical expressions:• not (negation, ¬)• or (disjunction, ∨)• if (implication, →)• any (universal quantification, ∀)• Indeterminate/underspecified description of a situation• Not easy to visualize (“Draw a picture of A man is not walking“)

27 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
H1. Some animals danced.
H2. Some grizzlies danced.
H3. Some bears moved.
H4. Some bears waltzed.

28 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
⇒ H1. Some animals danced.
H2. Some grizzlies danced.
H3. Some bears moved.
H4. Some bears waltzed.

28 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
⇒ H1. Some animals danced.
̸⇒ H2. Some grizzlies danced.
H3. Some bears moved.
H4. Some bears waltzed.

28 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
⇒ H1. Some animals danced.
̸⇒ H2. Some grizzlies danced.
⇒ H3. Some bears moved.
H4. Some bears waltzed.

28 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
⇒ H1. Some animals danced.
̸⇒ H2. Some grizzlies danced.
⇒ H3. Some bears moved.
̸⇒ H4. Some bears waltzed.

28 / 51

Monotonicity inference

Basic/general patterns of inferences triggered by logic features
P entails H= There is no situation in which P is true but H is false.
= The information in P already contains the information in H.
• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence? (Moss, 2014)
P: Some bears danced.
⇒ H1. Some animals danced.
̸⇒ H2. Some grizzlies danced.
⇒ H3. Some bears moved.
̸⇒ H4. Some bears waltzed.
We write: Some bears↑ danced↑
NP and VP in Some NP VP are upward monotonic
28 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
H1. No animals danced.
H2. No grizzlies danced.
H3. No bears moved.
H4. No bears waltzed.

29 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
̸⇒ H1. No animals danced.
H2. No grizzlies danced.
H3. No bears moved.
H4. No bears waltzed.

29 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
̸⇒ H1. No animals danced.
⇒ H2. No grizzlies danced.
H3. No bears moved.
H4. No bears waltzed.

29 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
̸⇒ H1. No animals danced.
⇒ H2. No grizzlies danced.
̸⇒ H3. No bears moved.
H4. No bears waltzed.

29 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
̸⇒ H1. No animals danced.
⇒ H2. No grizzlies danced.
̸⇒ H3. No bears moved.
⇒ H4. No bears waltzed.

29 / 51

Monotonicity inference• grizzly ≤ bear ≤ animal• waltz ≤ dance ≤ move

P entails which sentence?

P: No bears danced.
̸⇒ H1. No animals danced.
⇒ H2. No grizzlies danced.
̸⇒ H3. No bears moved.
⇒ H4. No bears waltzed.
We write: No bears↓ danced↓
NP and VP in No NP VP are downward monotonic• Logical words like some, no, every, any, not, if play a role indetermining the upward/downward monotonicity.

29 / 51

Bare NPs

For bare NPs (NPs without determiners), predicates play a crucial role.

tigress ≤ tiger ≤ animal
Tigers are striped.
⇒ Tigresses are striped.
̸⇒ Animals are striped.

Tigers are on the lawn.
̸⇒ Tigresses are on the lawn.
⇒ Animals are on the lawn.

Tigers↓ are striped. (individual-level predicate)
Tigers↑ are on the lawn. (stage-level predicate)• The basic patterns of monotonicity inferences are directlypredictable from logic-based MRs.

• Upward/downward monotonicity properties follow from theproperties of logical operators.
∃x(bear ↑ (x) ∧ dance↑ (x))¬∃x(bear ↓ (x) ∧ dance↓ (x))

30 / 51

Level 3: Advanced logic features
There are many linguistic phenomena that allegedly go beyond
standard first-order logic.
• Attitudes, modals and aspectual operators.
• Generalized/proportional quantifiers• Intensional adjectives• Comparative and superlatives• Other higher-order predicatesSome features:• Introducing intensionality (involving speaker’s perspectives,

mental states, etc.)• Quantifying over higher-order objects (objects other than entities)• Not directly formalizable in first-order logics

31 / 51

Attitudes, modals and temporal operators• Attitude predicates like know and believe take propositional

objects as argument.

• Inferential contrast between factive predicates (eg. know) andnon-factive predicate (eg. believe)• John knows that it is raining.

⇒ It is raining.

• John does not know that it is raining.

⇒ It is raining.

• John believes that it is raining.

̸⇒ It is raining.

• John does not believe that it is raining.

̸⇒ It is raining.

• modals: likely, probably, might, must, can. etc.

• aspectual operators: progressives, perfectives, etc.
32 / 51

Generalized quantifiers

Proportional quantifiers:• Most, half of, 70% of ...

Monotonicity properties:
Most students smoked.
Most students smoked.

̸⇒ ⇐
̸
⇐=

Most female student smoked.
Most student smoked in a building.

• But these quantifiers are known to be not

first-orderizable (Barwise and Cooper, 1981)

33 / 51

Adjectives: subsective and non-subsective

Subsective (intersective) adjective• Dumbo is a small elephant. small(dumbo) ∧ elephant(dumbo)⇒ Dumbo is an elephant. elephant(dumbo)Non-subsective adjective• This is a fake diamond.

̸⇒ This is a diamond.
⇒ This is not a diamond.

34 / 51

Comparatives• Alice is taller than Bob.

̸⇒ Alice is tall.

• Alice is taller than Bob.
• Bob is tall.

⇒ Alice is tall.

• Alice is taller than Bob.

• Bob is taller than Carol.

⇒ Alice is taller than Carol.

Question:• What are proper MRs for adjective constructions that are suitableto efficient inferences?

• How to give a compositional semantics of predicates tall and taller(how the meanings of tall and taller are related to each other?)

35 / 51

Some higher-order predicates• Higher-order predicates that apply to objects other than entities:rise, change, decrease• The price of gasoline is rising.

• The price of gasoline is 1,000 dollars.

̸⇒ 1,000 dollars are rising.

36 / 51

Logic-based Meaning Representations
Natural Logic

First-order logic(FOL)

Higher-order logic(HOL)• formalizes inferenceswith surface form
! only allows single
premise inferences(mononicity inference)• efficient provers exist• dominate computational
linguistics! limited expressive
power• high expressive power• dominate formal semantics! no general-purpose
efficient prover exists

more efficientless expressive
MacCartney (2009)less efficient
more expressive
Boxer (Bos 2008)

Mineshima et al. (2015)37 / 51

Logic-based Meaning Representations
Natural Logic

First-order logic(FOL)

Higher-order logic(HOL)• formalizes inferenceswith surface form
! only allows single
premise inferences(mononicity inference)• efficient provers exist• dominate computational
linguistics! limited expressive
power• high expressive power• dominate formal semantics! no general-purpose
efficient prover exists

more efficientless expressive
MacCartney (2009)less efficient
more expressive
Boxer (Bos 2008)

Mineshima et al. (2015)37 / 51

Logic-based Meaning Representations
Natural Logic

First-order logic(FOL)

Higher-order logic(HOL)• formalizes inferenceswith surface form
! only allows single
premise inferences(mononicity inference)• efficient provers exist• dominate computational
linguistics! limited expressive
power• high expressive power• dominate formal semantics! no general-purpose
efficient prover exists

more efficientless expressive
MacCartney (2009)less efficient
more expressive
Boxer (Bos 2008)

Mineshima et al. (2015)37 / 51

HOL as representation language
Higher-order constructions in natural languages
1 Generalized quantifiers
Most students work " most(λ.student(x), λx.work(x))
2 Modals
John might come " might(come(j))
3 Veridical and anti-veridical predicatesSomeone managed to come " ∃x(manage(x, come(x)))
Someone failed to come " ∃x(fail(x, come(x)))
4 Attitude verbs
John knows that some student came. "know(j, ∃x(student(x) ∧ come(x)))• Higher-order inference system implemented in Coq (Mineshima

et al., 2015)• Alternative: first-order decomposition/reification (Hobbs, 1985)

38 / 51

Natural Language Inference (Recognizing Textual
Entailment, RTE)
• Does P entail H?

P
H

Most cities in Japan prohibit smoking in restaurants.
Some cities in Japan do not allow smoking in public spaces.
Yes (entail)• The best way of testing an NLP system’s semantic capacity(Cooper et al. 1996)• Many applications in NLP• Question Answering,• Text Summarization• Fact validation/checking• etc.

39 / 51

Datasets for Recognizing Textual Entailment (RTE)• English:

DatasetFraCaS (Cooper et al., 1994)
PASCAL-RTE1–5 (Dagan et al. 2006)
SICK (Marelli et al., 2014)
SNLI (Bowman et al., 2015)
MultiNLI (Williams et al. 2017)

Size
346
7K
10K
570K
432K

Crowdsourcing√√√• Japanese:

DatasetJSeM
NTCIR RITE 1–2
Kyoto RTE dataset

Size
780
1,800
2,471

Crowdsourcing

40 / 51

FraCaS (Cooper et al. 1996)• Created by linguists in 1990s.

• Size: 346 problems• The inferences are divided into nine sections in terms of linguistic

phenomena:• Generalized quantifier, Plurals, Nominal anaphora, Ellipsis,
Adjective, Comparatives, Temporal reference, Verbs, Attitudes• Contains lots of logical expressions (at Level 2 and Level 3)• Lexical and world knowledge is mostly excluded• Contains multiple-premise inferences# premise
1
2
3
4
5

# problem
192
122
29
2
1

55.5%
35.3%
8.4%
0.6%
0.3%
41 / 51

FraCaS: Examples• The XML format was created by Bill MacCartney

https://nlp.stanford.edu/~
wcmac/downloads/

fracas-038 (Generalized quantifier) label: no (contradiction)
P: No delegate finished the report.
H: Some delegate finished the report on time.
fracas-084 (Plural) label: yes (entailment)
P: Either Smith, Jones or Anderson signed the contract.
H: If Smith and Anderson did not sign the contract, Jones signed the contract.
fracas-134 (Nominal Anaphora) label: yes (entailment)
P1: Every customer who owns a computer has a service contract for it.
P2: MFI is a customer that owns exactly one computer.
H: MFI has a service contract for all its computers.
42 / 51

Japanese Semantics Test Suite (JSeM)
Kawazoe et al. (2015)

http://researchmap.jp/community-inf/JSeM/• Translation of FraCaS (624 problems) and Japanese original ones
(166 problems)• Each problem is tagged with:• phenomena type (quantifier, adjective, negation, etc.)• inference type (logical entailment, presupposition)• single-premised (66%) and multi-premised (34%) problems

43 / 51

SICK (Sentences Involving Compositional Knowldedge)
SemEval14, Marelli et al. (2013)• Size: 4, 500/500/4, 927 for training, dev. and testing.

• Premise: taken from image captions in Flickr30k Corpus• Hyphothesis and Label: crowdsourcing and expert-check• contains only single-premise inferences• contains logical expressions at Level 2 (negation, disjunction,

quantifiers)• Both word-level and phrase-level paraphrases are required

44 / 51

SICK: Examples
SICK-506 (label: no)
P: A man wearing a dyed black shirt is sitting at the table and laughing.
H: There is no man wearing a shirt dyed black, sitting at the table andlaughing.
SICK-718 (label: unknown)
P: A few men in a competition are running outside.
H: A few men are running competitions outside.
SICK-3156 (label: yes)
P: A man is cutting a box.
H: A box is being cut by a man.
SICK-3668 (label: yes)
P: A man is strolling in the rain.
H: A man is walking in the rain.
45 / 51

SNLI
Bowman et al. (2015)• The Stanford Natural Language Inference (SNLI) Corpus• P: taken from image captions in Flickr30k Corpus• H and Label: crowdsourcing• contains only single-premise inferences• sentences are confined to descriptions of scenes, not containing

logical features (limited to Level 1)• largely limited to simple lexical inferences

label: entailment
P: A white dog with long hair jumps to catch a red and green toy.
H: An animal is jumping to catch an object.

46 / 51

MultiNLIWilliams et al. (2017)• The Multi-Genre Natural Language Inference (MultiNLI)

genre: Fiction, answer: entailment
P: He turned and saw Jon sleeping in his half-tent.
H: He saw Jon was asleep.
genre: telephone, answer: contradiction
P: someone else noticed it and i said well i guess that’s true and it was
somewhat melodious in other words it wasn’t just you know it was
really funny
H: No one noticed and it wasn’t funny at all.
• A set of linguistic phenomena tags are automatically assigned tothe development set (10K sentences):• quantifiers, belief verbs, time terms, conditionals, etc.

47 / 51

Summary• Compositional Semantics:• Meaning composition via CCG and Lambda Calculus• Meaning Representations:• Three levels of MRs for semantic composition:

Predicate-Argument Structure, Basic Logics and beyond• Event Semantics, First-order logic, and Higher-order logic• Inference: RTE datasets

48 / 51

AMi`Q/m+iBQM iQ ++;kHK#/

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

AMTmi, AM72`2M+2
SR aKQFBM; Bb T`Q?B#Bi2/ BM KQbi +BiB2bX> aKQFBM; Bb MQi HHQr2/ BM bQK2 +BiB2bX
h?2 bvbi2K ++2Tib #Qi? bBM;H2@T`2KBb2
M/ KmHiB@T`2KBb2 BM72`2M+2b

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM
*QK#BMiQ`v *i2;Q`BH :`KK`**: Uai22/KM- kyyyc "2FFB- kyRyV• ** T`b2` U*H`F M/ *m``M- kyydV- i`BM2/ QM**:#MF U>Q+F2MKB2` M/ ai22/KM- kyydV• CB;; ULQDB M/ JBvQ- kyR8V

S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22**: T`b2 i`22 7Q` 2+? b2Mi2M+2

aKQFBM;
LS

KQbi +BiB2b
BM
L
T`Q?B#Bi2/ ((a\LS)\(a\LS))/L>
a\LS(a\LS)\(a\LS)
Bb<(a\LS)/(a\LS)
a\LS
>
a\LS
<
a

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

a2KMiB+ +QKTQbBiBQM pB GK#/@+H+mHmb

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

avMi+iB+ *i2;Q`v , J2MBM;"/ : 7  : >" : 7

 :  "\ : 7<" : 7

:Bp2M  **:@i`22- i?2 b2KMiB+ `2T`2b2MiiBQM +M#2 /2`Bp2/ BM  7mHHv +QKTQbBiBQMH rvX

S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

a2KMiB+ `2T`2b2MiiBQM BM >PG

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

SR aKQFBM; Bb T`Q?B#Bi2/ BM KQbi +BiB2bX∃t(bKQFBM;(t) ∧KQbi(λv.+Biv(v), λv.T`Q?B#Bi2/(t) ∧ BM(t, v)))

> aKQFBM; Bb MQi HHQr2/ BM bQK2 +BiB2bX∃t(bKQFBM;(t) ∧∃v(+Biv(v) ∧ ¬HHQr2/(t) ∧ BM(t, v)))S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

>B;?2`@Q`/2` BM72`2M+2 bvbi2K
BKTH2K2Mi2/ QM *Q[

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

U*7X *?ixBFv`BFB/Bb M/ GmQ- kyR9V*Q[, BMi2`+iBp2 i?2Q`2K@T`Qp2` #b2/ QM?B;?2`@Q`/2` HQ;B+fKQ/2`M ivT2 i?2Q`v>PG tBQK, ∀6∀:(KQbi(6, :) → ∃t(6t ∧ :t))qQ`/L2i tBQK, ∀t(T`Q?B#Bi2/(t) → ¬HHQr2/(t))

S`Qp2`

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

++;kHK#/, a2KMiB+ S`b2` M/ AM72`2M+2 avbi2K?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

h2ti

**:
T`b2`

S`b2 i`22

PmiTmi, v2bfMQfmMFMQrM

a2KMiB+*QKTQbBiBQM

a2KMiB+`2T`2b2MiiBQM

SR ∃t(bKQFBM;(t) ∧KQbi(λv.+Biv(v), λv.T`Q?B#Bi2/(t) ∧ BM(t, v)))> ∃t(bKQFBM;(t) ∧S`Qp2`∃v(+Biv(v) ∧ ¬HHQr2/(t) ∧ BM(t, v)))

Mbr2` , u2b USR 2MiBHb >V

u2b U1MiBHV
LQ U*QMi`/B+iV
lMFMQrM

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v

r?Q

bim/2Mi
L

LS/L
LS

rQ`Fb
a\LS

(LS\LS)/(a\LS)

>

>

LS\LS

<

LS
a

Ç avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX

+QK2b
a\LS

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v

r?Q

bim/2MiL

LS/L(λ1t.1(t))(bim/2Mi)
LS

rQ`Fb
a\LS

(LS\LS)/(a\LS)

>

>

LS\LS

<

LS

+QK2b
a\LS

a

Ç avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX
Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v

r?Q

bim/2MiL

LS/L

λt.bim/2Mi(t)
LS

rQ`Fb
a\LS

(LS\LS)/(a\LS)

>

>

LS\LS

<

LS

+QK2b
a\LS

a

Ç avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX
Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX
Ç β@`2/m+iBQM rBi? H2KKb b `;mK2MibX

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v

r?Q

bim/2MiL

LS/L

λt.bim/2Mi(t)
LS

rQ`Fb

(LS\LS)/(a\LS)>a\LS
λZ.Z(λt.h`m2)(λt.rQ`F(t))
LS\LS

LS

>

+QK2b
<
a\LS
λZ.Z(λt.h`m2)(λt.+QK2(t))

aÇ avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX
Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX
Ç β@`2/m+iBQM rBi? H2KKb b `;mK2MibX
Ç a2KMiB+b KQ`2 BMi2`2biBM; 7Q` p2`#bX

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v
LS/L
λ6:>.∀t(6t ∧ :t → >t)LSr?Q

bim/2MiL

λt.bim/2Mi(t)(LS\LS)/(a\LS)λoZ6.Z(λt.(o(λ:>.>t) ∧ 6t))

>

rQ`Fb

a\LS
λZ.Z(λt.h`m2)(λt.rQ`F(t))

LS\LS
LS

>

+QK2b
<
a\LS
λZ.Z(λt.h`m2)(λt.+QK2(t))

aÇ avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX
Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX
Ç β@`2/m+iBQM rBi? H2KKb b `;mK2MibX
Ç a2KMiB+b KQ`2 BMi2`2biBM; 7Q` p2`#bX
Ç *HQb2/ rQ`/b, /B`2+i bbB;MK2MiX

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v
LS/L
λ6:>.∀t(6t ∧ :t → >t)LSr?Q

bim/2MiL

λt.bim/2Mi(t)(LS\LS)/(a\LS)λoZ6.Z(λt.(o(λ:>.>t) ∧ 6t))

>

LS\LS

λ:>.∀t(bim/2Mi(t) ∧ :t → >t)

rQ`Fb

a\LS
λZ.Z(λt.h`m2)(λt.rQ`F(t))

LS

>

+QK2b
<
a\LS
λZ.Z(λt.h`m2)(λt.+QK2(t))

aÇ avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX
Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX
Ç β@`2/m+iBQM rBi? H2KKb b `;mK2MibX
Ç a2KMiB+b KQ`2 BMi2`2biBM; 7Q` p2`#bX
Ç *HQb2/ rQ`/b, /B`2+i bbB;MK2MiX
Ç a2KMiB+ +QKTQbBiBQM 7`QK H2p2b iQ `QQiX

a2KMiB+ +QKTQbBiBQM QM **: i`22
1p2`v
LS/L
λ6:>.∀t(6t ∧ :t → >t)LSr?Q

bim/2MiL

λt.bim/2Mi(t)(LS\LS)/(a\LS)λoZ6.Z(λt.(o(λ:>.>t) ∧ 6t))

>

rQ`Fb

a\LS
λZ.Z(λt.h`m2)(λt.rQ`F(t))

LS\LSλZ6.Z(λt.(rQ`F(t) ∧ 6t))λ:>.∀t(bim/2Mi(t) ∧ :t → >t)LS

λ6>.∀t(bim/2Mi(t) ∧ rQ`F(t) ∧ 6t → >t)

>

+QK2b
<
a\LS
λZ.Z(λt.h`m2)(λt.+QK2(t))

a∀t(bim/2Mi(t) ∧ rQ`F(t) ∧ h`m2 → +QK2(t))Ç avMi+iB+ +i2;Q`B2b M/ `mH2b BM/B+i2 +QKTQbBiBQMX

Ç PT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`B2b Ki+? bvMi+iB+ +i2;Q`B2bX
Ç β@`2/m+iBQM rBi? H2KKb b `;mK2MibX
Ç a2KMiB+b KQ`2 BMi2`2biBM; 7Q` p2`#bX
Ç *HQb2/ rQ`/b, /B`2+i bbB;MK2MiX
Ç a2KMiB+ +QKTQbBiBQM 7`QK H2p2b iQ `QQiX
Ç GQ;B+H K2MBM; `2T`2b2MiiBQM Q7 i?2 b2Mi2M+2 i i?2 `QQiX

G2tB+H 2Mi`B2b
R

6Q` +HQb2/ rQ`/b, H2tB+H 2Mi`B2b /B`2+iHv bbB;M2/ iQ bm`7+2 7Q`K U
HBKBi2/ MmK#2` Q7 ;`KKiB+H M/ HQ;B+H 2tT`2bbBQMbV, 3y 2Mi`B2b
1tKTH2
Ç +i2;Q`v, LS/L
Ç b2KMiB+b, λ6λ:λ>.∀t(6t ∧ :t → >)Ç bm`7, 2p2`v

k

6Q` QT2M rQ`/b, b+?2KiB+ H2tB+H 2Mi`v Ub2KMiB+ i2KTHi2bV
bbB;M2/ iQ bvMi+iB+ +i2;Q`B2b, 8d 2Mi`B2b
1tKTH2
Ç +i2;Q`v, L
Ç b2KMiB+b, λ1λt.1(t)ǳ1Ǵ Bb  TQbBiBQM BM r?B+?  T`iB+mH` H2tB+H Bi2K TT2`bX

++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,

++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,Ç O Tvi?QM b2KT`b2XTv ++;i`22bXtKH i2KTHi2bXvKH b2KMiB+bXtKH

R
k
j
9
8
e
d
3
N
Ry
RR
Rk
Rj
R9
R8
Re
Rd
R3
RN
ky
kR
kk
kj
k9
k8
ke

−3Ƕ \=

I\ tKH p 2 ` b B Q M4Ƕ R X y Ƕ 2M+Q /BM;4Ƕ m i 7
I` Q Q i=
I/Q+mK2Mi=
Ib 2 M i 2 M + 2 b=
Ib 2 M i 2 M + 2=
Ii Q F 2 M b=

IiQF2M B /4ǴiynyǴ TQb4Ǵ.hǴ

+  i4ǴLS( M# ) fLǴb m ` 74ǴaQK2Ǵ

#b24ǴbQK2Ǵf=IiQF2M B /4ǴiynRǴ TQb4ǴLLǴ+  i4ǴLǴb m ` 74ǴrQKMǴ#b24ǴrQKMǴf=I X X X f=
If i Q F 2 M b=
I++; ` Q Q i4Ǵ bynbTy Ǵ B /4Ǵ byn++;y Ǵ=
IbTM B /4Ǵ bynbTy Ǵ + ? B H /4Ǵ bynbTR bynbTN Ǵ +  i 2 ; Q ` v4Ǵa ( / + H4i ` m 2 ) Ǵ` m H 24Ǵ `T Ǵf=

IbTM B /4Ǵ bynbTR Ǵ + ? B H /4Ǵ bynbTk bynbT8 Ǵ +  i 2 ; Q ` v4Ǵa ( / + H4i ` m 2 ) Ǵ` m H 24Ǵ#Ǵf=I X X X=
If ++;=
Ib 2 K  M i B + b b i  i m b4Ǵ b m + + 2 b b Ǵ ` Q Q i4Ǵ bynbTy Ǵ=
IbTM B /4Ǵ bynbTy Ǵ + ? B H /4Ǵ bynbTR bynbTN Ǵ
b2K4Ǵ 2 t B b i b t X U nrQKMU t V  h`m2S  2 t B b i b xR X U ni2 U xR V  h`m2S  nQ`/2` U t - xR V V V Ǵf=
IbTM B /4Ǵ bynbT9 Ǵ i v T 24ǴnrQKM , 1 M i B i v
b2K4Ǵ$t X nrQKMU t V Ǵf=I X X X=
If b 2 K  M i B + b=
If b 2 M i 2 M + 2=
If b 2 M i 2 M + 2 b=
If/Q+mK2Mi=
If ` Q Q i=−= S`QT Ǵ++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,Ç O Tvi?QM b2KT`b2XTv ++;i`22bXtKH i2KTHi2bXvKH b2KMiB+bXtKH
Ç O Tvi?QM pBbmHBx2XTv b2KMiB+bXtKH = b2KMiB+bX?iKH

++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,Ç O Tvi?QM b2KT`b2XTv ++;i`22bXtKH i2KTHi2bXvKH b2KMiB+bXtKH
Ç O Tvi?QM pBbmHBx2XTv b2KMiB+bXtKH = b2KMiB+bX?iKHÇ O Tvi?QM T`Qp2XTv b2KMiB+bXtKH

++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,Ç O Tvi?QM b2KT`b2XTv ++;i`22bXtKH i2KTHi2bXvKH b2KMiB+bXtKH
Ç O Tvi?QM pBbmHBx2XTv b2KMiB+bXtKH = b2KMiB+bX?iKHÇ O Tvi?QM T`Qp2XTv b2KMiB+bXtKHÇ 1bv iQ 2ti2M/ U/2+H`iBp2VX− b2KMiB+b : λ@7Q`KmH+i2;Q`v : bvMi+iB+n+i2;Q`v+QM/k : pHm2k
+QM/B : pHm2B

++;kHK#/,  72r KQ`2 rQ`/b?iiTb,ff;Bi?m#X+QKfKvMHTf++;kHK#/

Ç Sm#HB+Hv pBH#H2 M/ QT2M@bQm`+2/X
Ç 1bv iQ mb2 UbBKTH2 T`Q;`KbV,Ç O Tvi?QM b2KT`b2XTv ++;i`22bXtKH i2KTHi2bXvKH b2KMiB+bXtKH
Ç O Tvi?QM pBbmHBx2XTv b2KMiB+bXtKH = b2KMiB+bX?iKHÇ O Tvi?QM T`Qp2XTv b2KMiB+bXtKHÇ 1bv iQ 2ti2M/ U/2+H`iBp2VX
Ç 1bv iQ T`Q+2bb UsJG QmiTmiVX

_2+Q;MBxBM; h2timH 1MiBHK2Mi

_2+Q;MBxBM; h2timH 1MiBHK2Mi
Ç .Q2b S`2KBb2 S 2MiBH >vTQi?2bBb >\S>

aKQFBM; BM `2bim`Mib Bb T`Q?B#Bi2/ #v Hr BM KQbi +BiB2b BM CTMX
aKQFBM; BM Tm#HB+ bT+2b Bb MQi HHQr2/ BM bQK2 +BiB2bX
u2b U1MiBHK2MiV

_2+Q;MBxBM; h2timH 1MiBHK2Mi
Ç .Q2b S`2KBb2 S 2MiBH >vTQi?2bBb >\S>

aKQFBM; BM `2bim`Mib Bb T`Q?B#Bi2/ #v Hr BM KQbi +BiB2b BM CTMX
aKQFBM; BM Tm#HB+ bT+2b Bb MQi HHQr2/ BM bQK2 +BiB2bX
u2b U1MiBHK2MiV

Ç h?2 #2bi rv Q7 i2biBM; M LGS bvbi2KǶb b2KMiB+ +T+Biv U*QQT2`

2i HX RNNeVÇ JMv TTHB+iBQM `2b UZm2biBQM Mbr2`BM;- J+?BM2 h`MbHiBQM- 2i+XV

_2+Q;MBxBM; h2timH 1MiBHK2Mi
Ç .Q2b S`2KBb2 S 2MiBH >vTQi?2bBb >\S>

aKQFBM; BM `2bim`Mib Bb T`Q?B#Bi2/ #v Hr BM KQbi +BiB2b BM CTMX
aKQFBM; BM Tm#HB+ bT+2b Bb MQi HHQr2/ BM bQK2 +BiB2bX
u2b U1MiBHK2MiV

Ç h?2 #2bi rv Q7 i2biBM; M LGS bvbi2KǶb b2KMiB+ +T+Biv U*QQT2`

2i HX RNNeVÇ JMv TTHB+iBQM `2b UZm2biBQM Mbr2`BM;- J+?BM2 h`MbHiBQM- 2i+XVÇ `2H2pMi 7+iQ`b,

1. bvMit
2. HQ;B+H rQ`/b, KQbi- MQi- bQK2- 2p2`v

GQ;B+Hf*QKTQbBiBQMH b2KMiB+b

_2+Q;MBxBM; h2timH 1MiBHK2Mi
Ç .Q2b S`2KBb2 S 2MiBH >vTQi?2bBb >\S>

aKQFBM; BM `2bim`Mib Bb T`Q?B#Bi2/ #v Hr BM KQbi +BiB2b BM CTMX
aKQFBM; BM Tm#HB+ bT+2b Bb MQi HHQr2/ BM bQK2 +BiB2bX
u2b U1MiBHK2MiV

Ç h?2 #2bi rv Q7 i2biBM; M LGS bvbi2KǶb b2KMiB+ +T+Biv U*QQT2`

2i HX RNNeVÇ JMv TTHB+iBQM `2b UZm2biBQM Mbr2`BM;- J+?BM2 h`MbHiBQM- 2i+XVÇ `2H2pMi 7+iQ`b,

1. bvMit
2. HQ;B+H rQ`/b, KQbi- MQi- bQK2- 2p2`v

GQ;B+Hf*QKTQbBiBQMH b2KMiB+b

3. +QMi2Mi rQ`/b,`2bim`Mi → Tm#HB+n bT+2
T`Q?B#Bi2/ → ¬ HHQr2/

G2tB+H EMQrH2/;2AMi`Q/m+BM; G2tB+H EMQrH2/;2AMi`Q/m+iBQM
GQ;B+ bQK2iBK2b Bb MQi 2MQm;?
h,

K2M `2 brBM; HQ;bX∃t.(KM(t) ∧ ∃v.(HQ;(v) ∧ br(t, v))>,

K2M `2 +miiBM; rQQ/X∃t.(KM(t) ∧ ∃v.(rQQ/(v) ∧ +mi(t, v))

AMi`Q/m+iBQM
GQ;B+ bQK2iBK2b Bb MQi 2MQm;?
h,

K2M `2 brBM; HQ;bX∃t.(KM(t) ∧ ∃v.(HQ;(v) ∧ br(t, v))>,

K2M `2 +miiBM; rQQ/X∃t.(KM(t) ∧ ∃v.(rQQ/(v) ∧ +mi(t, v))

J2i?Q/, iQ BMD2+i H2tB+H FMQrH2/;2 BMiQ i?2 T`QQ7X
Ç qQ`/ `2HiBQMb +M #2 7QmM/ BM QMiQHQ;B2b U2X;X qQ`/L2i- 2i+XV∀t∀v.br(t, v) → +mi(t, v)∀t.HQ;(t) → rQQ/(t)Lśp2 BMD2+iBQM Q7 H2tB+H FMQrH2;2_mMMBM; 2tKTH2,∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )

h,



#H+F

M/

r?Bi2

/Q;

MTb X

>,



#H+F

M/

r?Bi2

/Q;

bH22Tb X∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç P#iBM b2KMiB+ `2T`2b2MiiBQMX

Lśp2 BMD2+iBQM Q7 H2tB+H FMQrH2;2_mMMBM; 2tKTH2,∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )

h,



#H+F

M/

r?Bi2

/Q;

MTb X

>,



#H+F

M/

r?Bi2

/Q;

bH22Tb X∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç A/2MiB7v +QMi2MifBMi2`2biBM; rQ`/bX

Lśp2 BMD2+iBQM Q7 H2tB+H FMQrH2;2_mMMBM; 2tKTH2,∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )

h,



#H+F

M/

r?Bi2

/Q;

MTb X

>,



#H+F

M/

r?Bi2

/Q;

bH22Tb X∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç 1MmK2`i2 TQbbB#H2 `2HiBQMbX

Lśp2 BMD2+iBQM Q7 H2tB+H FMQrH2;2_mMMBM; 2tKTH2,∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )

h,



#H+F

M/

r?Bi2

/Q;

MTb X

>,



#H+F

M/

r?Bi2

/Q;

bH22Tb X∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç a2H2+ifT`2/B+i `2HiBQMb ++Q`/BM; iQ QMiQHQ;v Q` +HbbB}2`,
Ç ∀t.#H+F(t) → ¬ r?Bi2(t)Ç ∀t.r?Bi2(t) → ¬ #H+F(t)Ç ∀p.MT(p) → bH22T(p)Lśp2 BMD2+iBQM Q7 H2tB+H FMQrH2;2_mMMBM; 2tKTH2,∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )

h,



#H+F

M/

r?Bi2

/Q;

MTb X

>,



#H+F

M/

r?Bi2

/Q;

bH22Tb X∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç AMb2`i FMQrH2/;2- `mM T`QQ7X
Ç XXX M/ TQbbB#Hv ;2i i?2 r`QM; Mbr2`XÇ h?Bb T`Q#H2K Bb ;;`pi2/ 7Q` HQM;2` b2Mi2M+2bX

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç .2+QKTQb2 h M/ > BMiQ,Ç SQQH Q7 HQ;B+H T`2KBb2b SX
Ç GBbi Q7 bm#@;QHb :XS`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç .2+QKTQb2 h M/ > BMiQ,Ç SQQH Q7 HQ;B+H T`2KBb2b SX
Ç GBbi Q7 bm#@;QHb :XÇ o`B#H2 mMB}+iBQM t2 := t1 X
Ç S`Qp2 ;1 , ;2 M/ ;3 XXX
Ç XXX mbBM; T1 , T2 M/ T3 X

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç .2+QKTQb2 h M/ > BMiQ,Ç SQQH Q7 HQ;B+H T`2KBb2b SX
Ç GBbi Q7 bm#@;QHb :XÇ o`B#H2 mMB}+iBQM t2 := t1 X
Ç S`Qp2 ;1 , ;2 M/ ;3 XXX
Ç XXX mbBM; T1 , T2 M/ T3 XÇ o`B#H2 mMB}+iBQM p2 := p1 X
Ç S`Qp2 ;4 mbBM; T4 X

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç .2+QKTQb2 h M/ > BMiQ,Ç SQQH Q7 HQ;B+H T`2KBb2b SX
Ç GBbi Q7 bm#@;QHb :XÇ o`B#H2 mMB}+iBQM t2 := t1 X
Ç S`Qp2 ;1 , ;2 M/ ;3 XXX
Ç XXX mbBM; T1 , T2 M/ T3 XÇ o`B#H2 mMB}+iBQM p2 := p1 X
Ç S`Qp2 ;4 mbBM; T4 X
Ç AMD2+i tBQK ∀p.MT(p) → bH22T(p)XÇ MT(p1 ) M/ bH22T(p1 ) b?`2p`B#H2X
Ç MT@bH22T ∈ qQ`/L2iX
Ç *QMiBMm2 T`QQ7X

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t2 p2 (/Q;(t2 ) ∧ r?Bi2(t2 ) ∧ #H+F(t2 ) ∧ bH22T(p2 ) ∧ am#D(p2 ) = t2 )
Ç .2+QKTQb2 h M/ > BMiQ,Ç SQQH Q7 HQ;B+H T`2KBb2b SX
Ç GBbi Q7 bm#@;QHb :XÇ o`B#H2 mMB}+iBQM t2 := t1 X
Ç S`Qp2 ;1 , ;2 M/ ;3 XXX
Ç XXX mbBM; T1 , T2 M/ T3 XÇ o`B#H2 mMB}+iBQM p2 := p1 X
Ç S`Qp2 ;4 mbBM; T4 X
Ç AMD2+i tBQK ∀p.MT(p) → bH22T(p)XÇ MT(p1 ) M/ bH22T(p1 ) b?`2p`B#H2X
Ç MT@bH22T ∈ qQ`/L2iX
Ç *QMiBMm2 T`QQ7X

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ bH22T(p1 ) ∧ am#D(p1 ) = t1 )

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ bH22T(p1 ) ∧ am#D(p1 ) = t1 )Ç o`B#H2 mMB}+iBQM 7`QK T`QQ7XXXS`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ bH22T(p1 ) ∧ am#D(p1 ) = t1 )Ç o`B#H2 mMB}+iBQM 7`QK T`QQ7XXX
Ç .2}M2b M HB;MK2Mi #2ir22M HQ;B+ T`2/B+i2bX
Ç JQbi i?2Q`2K T`Qp2`b T2`7Q`K #+Fi`+FBM; BM i?2 b2`+? Q7 #2bi
HB;MK2MiX

S`QpBM; bi`i2;v M/ tBQK +QMbi`m+iBQM
h : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ MT(p1 ) ∧ am#D(p1 ) = t1 )> : ∃t1 p1 (/Q;(t1 ) ∧ r?Bi2(t1 ) ∧ #H+F(t1 ) ∧ bH22T(p1 ) ∧ am#D(p1 ) = t1 )Ç o`B#H2 mMB}+iBQM 7`QK T`QQ7XXX
Ç .2}M2b M HB;MK2Mi #2ir22M HQ;B+ T`2/B+i2bX
Ç JQbi i?2Q`2K T`Qp2`b T2`7Q`K #+Fi`+FBM; BM i?2 b2`+? Q7 #2bi
HB;MK2MiX
Ç "2ii2` B/2MiB7v HQ;B+fi2timH `2HiBQMb,
Ç ∀p.MT(p) → bH22T(p)X

avbi2KR

hQF2MBx2 h M/ >XkavMi+iB+ T`bBM; rBi? ** M/ 1bv**:X

P#iBM J2MBM; _2T`2b2MiiBQMb rBi? ++;kHK#/X
9 JQMBiQ` T`QQ7 M/ BMD2+i tBQKb QM@/2KM/,jÇ bvMQMvKv U2X;X ?Qmb2 → ?QK2VÇ ?vT2`MvKv U2X;X b2 → ri2`VÇ /D2+iBpH bBKBH`Biv U2X;X ?m;2 → #B;VÇ /2`BpiBQMHHv `2Hi2/ 7Q`Kb U2X;X ++QKKQ/iBM; → ++QKKQ/iBQMVÇ BM~2+iBQM `2HiBQMb U2X;X rQQ/2/ → rQQ/VÇ MiQMvKv `2HiBQMb U2X;X #B; → ¬bKHHVX

1pHmiBQM
aA*E /ib2i
Ç aBx2, 4, 500/500/4, 927 7Q` i`BMBM;- /2pX M/ i2biBM;X
Ç G#2H /Bbi`B#miBQM, .29/.15/.56 7Q` v2bfMQfmMFX
Ç #Qmi 212, 000 `mMMBM; rQ`/bX

Ç p2`;2 T`2KBb2 M/ +QM+HmbBQM H2M;i?, 10.6X
Ç LQ T`K2i2` 2biBKiBQMX

1pHmiBQM
aA*E /ib2i
Ç aBx2, 4, 500/500/4, 927 7Q` i`BMBM;- /2pX M/ i2biBM;X
Ç G#2H /Bbi`B#miBQM, .29/.15/.56 7Q` v2bfMQfmMFX
Ç #Qmi 212, 000 `mMMBM; rQ`/bX

Ç p2`;2 T`2KBb2 M/ +QM+HmbBQM H2M;i?, 10.6X
Ç LQ T`K2i2` 2biBKiBQMX

1tKTH2b,
S`Q#H2K A.
R9Rk
9RR9
dR3

h@> TB`bh, J2M `2 brBM; HQ;b X>, J2M `2 +miiBM; rQQ/ X
h, h?2`2 Bb MQ KM 2iBM; 7QQ/ X>,  KM Bb 2iBM;  TBxx Xh,  72r K2M BM  +QKT2iBiBQM `2 `mMMBM; QmibB/2 X>,  72r K2M `2 `mMMBM; +QKT2iBiBQMb QmibB/2 X

1MiBHK2Mi
u2b
LQ
lMFMQrM

1pHmiBQM
_2bmHib,
avbi2K"b2HBM2 UKDQ`BivV

S`2+X
−

_2+X
−

++X
56.69

1pHmiBQM
_2bmHib,
avbi2K"b2HBM2 UKDQ`BivV
JGL
Lmi+`+F2`
Lmi+`+F2`@qL
Lmi+`+F2`@qL@SS."
JGL@qL@SS."
GM;S`Q >v#`B/@3yyh?2 J2MBM; 6+iQ`v

S`2+X
−
−
−
−
−
−
97.95
93.63

_2+X
−
−
−
−
−
−
58.11
60.64

++X
56.69
73.40
74.30
77.50
78.60
80.40
81.35
81.60

1pHmiBQM
_2bmHib,
avbi2K"b2HBM2 UKDQ`BivV
JGL
Lmi+`+F2`
Lmi+`+F2`@qL
Lmi+`+F2`@qL@SS."
JGL@qL@SS."
GM;S`Q >v#`B/@3yyh?2 J2MBM; 6+iQ`v
LQ tBQKb
Lśp2
aSa-qL-oP

S`2+X
−
−
−
−
−
−
97.95
93.63
98.90
92.99
97.04

_2+X
−
−
−
−
−
−
58.11
60.64
46.48
59.70
63.64

++X
56.69
73.40
74.30
77.50
78.60
80.40
81.35
81.60
76.65
80.98
3j.Rj

1pHmiBQM
_2bmHib,
avbi2K"b2HBM2 UKDQ`BivV
JGL
Lmi+`+F2`
Lmi+`+F2`@qL
Lmi+`+F2`@qL@SS."
JGL@qL@SS."
GM;S`Q >v#`B/@3yyh?2 J2MBM; 6+iQ`v
LQ tBQKb
Lśp2
aSa-qL-oP
a2KMiBEGl1
lLG@LGS
1*Ll
AHHBMQBb@G>
JGL@2+HbbB7 U*GkyReV
uBM@a+?mix2 U1*GkyRdV

S`2+X
−
−
−
−
−
−
97.95
93.63
98.90
92.99
97.04
85.40
81.99
84.37
81.56
−
−

_2+X
−
−
−
−
−
−
58.11
60.64
46.48
59.70
63.64
69.63
76.80
74.37
81.87
−
−

++X
56.69
73.40
74.30
77.50
78.60
80.40
81.35
81.60
76.65
80.98
3j.Rj
82.32
83.05
83.64
84.57
85.10
3d.Ry

1``Q` MHvbBb
UKQ`2 +QKTH2t 2tKTH2b BM #+F@mT bHB/2VS`Q#X A.
R9Rk
k9y9
k3N8

h@> TB`bh, J2M `2 brBM; HQ;b X>, J2M `2 +miiBM; rQQ/ X
h, h?2 H/v Bb bHB+BM;  iQKiQ X>, h?2`2 Bb MQ QM2 +miiBM;  iQKiQ X
h, h?2 KM BbMǶi HB7iBM; r2B;?ib X>, h?2 KM Bb HB7iBM; #`#2HHb X:QH/

avbi2K

u2b

u2b

LQ

LQ

LQ

LQ

tBQKb M22/2/∀p.br(p) → +mi(p)∀t.HQ;(t) → rQQ/(t)∀p.bHB+2(p) → +mi(p)∀t.r2B;?i(t) → #`#2HH(t)1``Q` MHvbBb
UKQ`2 +QKTH2t 2tKTH2b BM #+F@mT bHB/2VS`Q#X A.
R9Rk
k9y9
k3N8
8jy

h@> TB`bh, J2M `2 brBM; HQ;b X>, J2M `2 +miiBM; rQQ/ X
h, h?2 H/v Bb bHB+BM;  iQKiQ X>, h?2`2 Bb MQ QM2 +miiBM;  iQKiQ X
h, h?2 KM BbMǶi HB7iBM; r2B;?ib X>, h?2 KM Bb HB7iBM; #`#2HHb X
h,  #BF2` Bb r2`BM; ;2` r?B+? Bb #H+F X>,  #BF2` r2`BM; #H+F Bb #`2FBM; i?2 ;2`b X

:QH/

avbi2K

u2b

u2b

LQ

LQ

LQ

LQ

lMF

u2b

tBQKb M22/2/∀p.br(p) → +mi(p)∀t.HQ;(t) → rQQ/(t)∀p.bHB+2(p) → +mi(p)∀t.r2B;?i(t) → #`#2HH(t)1``Q` MHvbBb
UKQ`2 +QKTH2t 2tKTH2b BM #+F@mT bHB/2VS`Q#X A.
R9Rk
k9y9
k3N8
8jy
R9N8
Rkee
kRee
j39

h@> TB`bh, J2M `2 brBM; HQ;b X>, J2M `2 +miiBM; rQQ/ X
h, h?2 H/v Bb bHB+BM;  iQKiQ X>, h?2`2 Bb MQ QM2 +miiBM;  iQKiQ X
h, h?2 KM BbMǶi HB7iBM; r2B;?ib X>, h?2 KM Bb HB7iBM; #`#2HHb X
h,  #BF2` Bb r2`BM; ;2` r?B+? Bb #H+F X>,  #BF2` r2`BM; #H+F Bb #`2FBM; i?2 ;2`b Xh,  KM Bb THvBM;  ;mBi` X>,  KM Bb bi`mKKBM;  ;mBi` Xh,  #M/ Bb THvBM; QM  bi;2 X>,  #M/ Bb THvBM; QMbi;2 Xh,  rQKM Bb b2rBM; rBi?  K+?BM2 X>,  rQKM Bb mbBM;  K+?BM2 K/2 7Q` b2rBM; X
h,  r?Bi2 M/ iM /Q; Bb `mMMBM; i?`Qm;?
i?2 iHH M/ ;`22M ;`bb X>,  r?Bi2 M/ iM /Q; Bb `mMMBM; i?`Qm;?  }2H/ X:QH/

avbi2Ku2b

u2b

tBQKb M22/2/∀p.br(p) → +mi(p)∀t.HQ;(t) → rQQ/(t)

LQ

LQ

LQ

LQ

lMF

u2b

u2b

lMF

∀p.THv(p) → bi`mK(p)

u2b

lMF

ǳQM  bi;2Ǵ → ǳQMbi;2Ǵ

u2b

lMF

u2b

lMF

∀p.bHB+2(p) → +mi(p)∀t.r2B;?i(t) → #`#2HH(t)ǳb2rBM; rBi?  K+?BM2Ǵ →ǳmbBM;  K+?BM2 K/2 7Q` b2rBM;Ǵ
ǳiHH M/ ;`22M ;`bbǴ → ǳ}2H/Ǵ

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb_2+Q;MBxBM; T?`b2 2MiBHK2Mib Bb HbQ M2+2bb`v5h,

K2M rHF BM i?2 iHH M/ ;`22M ;`bbX∃t.(KM(t) ∧ ∃v.(iHH(v) ∧ ;`22M(v) ∧ ;`bb(v) ∧ rHF(t, v))>,

K2M rHF BM i?2 }2H/X∃t.(KM(t) ∧ ∃v.(7B2H/(v) ∧ rHF(t, v))

S`Q#H2K,
Ç am+? FMQrH2/;2 +M MQi #2 7QmM/ BM /i#b2b U2X;X qQ`/L2i-

SS."VX

Ç a2KMiB+ `2Hi2/M2bb ̸= b2KMiB+ 2MiBHK2MiX
Ç .Bbi`B#miBQMH TT`Q+?2b U2X;X rQ`/kp2+V `2 MQi 2z2+iBp2,
Ç TBMQ 4⇒
̸;mBi`- +i 4⇏/Q;S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb:2i pBbmH /2MQiiBQMb Q7 T?`b2b M/ +QKT`2 BK;2bXh,

K2M rHF BM i?2 iHH M/ ;`22M ;`bbX>,

K2M rHF BM i?2 }2H/X

iHH M/ ;`22M ;`bb}2H/

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb:2i pBbmH /2MQiiBQMb Q7 T?`b2b M/ +QKT`2 BK;2bXh,

>2 +?ib rBi? ?Bb rB72 pB BMi2`M2i +K2`X>,>2 +?ib rBi? ?Bb rB72 pB r2#+KX
BMi2`M2i +K2`

r2#+KS?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
ai2T R, T?`b2 TB` B/2MiB}+iBQM

Ç A/2MiB7v 2tKTH2b Q7 T?`b2 2[mBpH2M+2bX

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
ai2T k, Q#iBM pBbmH /2MQiiBQMb

Ç Zm2`v BK;2b mbBM; T?`b2bX

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
ai2T j, G2`M _h1 *HbbB}2`

Ç G2`M T`K2i2`b Q7 _h1 +HbbB}2`X

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
ai2T 9, AMi2;`i2 BMiQ _h1 TBT2HBM2

Ç AMi2;`i2 QM _h1 TBT2HBM2 M/ 2pHmi2X

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb

Ç a2H2+i #2bi M/ rQ`bi T?`b2 TB` ++Q`/BM; iQ,

b+Q`2(i, ?) =1 !
Kt 7(Bi , B? )|A? | ? BiF ∈Ai F H
BH ∈A?

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb_2bmHib r?2M mbBM; pBbmH /2MQiiBQMb
avbi2K++;kHK#/ Y BK;2b++;kHK#/- QMHv i2ti
G>- i2ti Y BK;2bG>- QMHv i2ti
"b2HBM2 UKDQ`BivV

S`2+X
90.24
96.95
−
−
−

_2+X
71.08
62.65
−
−
−

++X
39.kN
83.13
82.70
81.50
56.69

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
1tKTH2bh`m2 TQbBiBp2,

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
1tKTH2b6Hb2 TQbBiBp2,

S?`bH 1MiBHK2Mib rBi? oBbmH .2MQiiBQMb
1tKTH2b6Hb2 M2;iBp2,h?MF vQm5

_M hBM- EQDB JBM2b?BK- Sb+mH J`iőM2x@:ƦK2xX

Reference I
Ajdukiewicz, K. (1935) “Die syntaktische Konnexit/”at”, Studia Philosophica 1,
pp.1–27.
Bar-Hillel, Y. (1953) “A quasi-arithmetical notation for syntactic description”,
Language 29(1), pp.47–58.
Barwise, J. and R. Cooper. (1981) “Generalized quantifiers and natural
language”, Linguistics and Philosophy 4(2), pp.159–219.
Bowman, S. R., G. Angeli, C. Potts, and C. D. Manning. (2015) “A large
annotated corpus for learning natural language inference”, In theProceedings of Proceedings of the 2015 Conference on Empirical Methods
in Natural Language Processing (EMNLP). Association for Computational
Linguistics.
Cooper, R., R. Crouch, J. van Eijck, C. Fox, J. van Genabith, J. Jaspers, H.
Kamp, M. Pinkal, M. Poesio, S. Pulman, et al. (1994) “FraCaS – A
Framework for Computational Semantics”, Deliverable D16.
Hobbs, J. R. (1985) “Ontological promiscuity”, In the Proceedings ofProceedings of the 23rd annual meeting on Association for Computational
Linguistics. pp.60–69.
49 / 51Reference II
Kamp, H. and U. Reyle. (1993) From discourse to logic: An introduction tomodeltheoretic semantics of natural language, formal logic and DRT.
Kluwer, Dordrecht.
Kawazoe, A., R. Tanaka, K. Mineshima, and D. Bekki. (2015) “An Inference
Problem Set for Evaluating Semantic Theories and Semantic Processing
Systems for Japanese”, In the Proceedings of Proceedings of LENLS12.
pp.67–73.
Marelli, M., S. Menini, M. Baroni, L. Bentivogli, R. Bernardi, and R.
Zamparelli. (2014) “A SICK cure for the evaluation of compositional
distributional semantic models.”, In the Proceedings of Proceedings of
LREC2014. pp.216–223.
Mineshima, K., P. Martı́nez-Gómez, Y. Miyao, and D. Bekki. (2015)“Higher-order logical inference with compositional semantics”, In theProceedings of Proceedings of the 2015 Conference on Empirical Methods
in Natural Language Processing. pp.2055–2061.
Moss, L. (2014) “Natural Logic”. NASSLLI 2014, Lecture slides.
Parsons, T. (1990) Events in the Semantics of English. MIT Press.
50 / 51Reference III

Steedman, M. (2000) The Syntactic Process. MIT Press.
Steedman, M. (2012) Taking scope: The natural semantics of quantifiers. MIT
Press.

51 / 51