Semantic Theory Lecture 2: Type theory - Universität des Saarlandes

[Pages:22]Semantic Theory Lecture 2: Type theory

M. Pinkal / A. Koller Summer 2006

Logic as a framework for NL semantics

? Approximate NL meaning as truth conditions. ? Logic supports precise, consistent and controlled

meaning representation via truth-conditional interpretation. ? Logic provides deduction systems to model inference processes, controlled through a formal entailment concept. ? Logic supports uniform modelling of the semantic composition process.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

2

1

Logic as a framework for NL semantics

? Approximate NL meaning as truth conditions. ? Logic supports precise, consistent and controlled

meaning representation via truth-conditional interpretation. ? Logic provides deduction systems to model inference processes, controlled through a formal entailment concept. ? Logic supports uniform modelling of the semantic composition process.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

3

Outline

? A reminder: First-order predicate logic (FOL). ? The limits of FOL as a formalism for semantic

representations. ? Type theory. ? Modal operators in logic.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

4

2

Dolphins

Dolphins are mammals, not fish. d (dolphin(d)mammal(d) ?fish(d))

Dolphins live in pods. d (dolphin(d) x (pod(p) live-in (d,p))

Dolphins give birth to one baby at a time. d (dolphin(d) x y t (give-birth-to (d,x,t) give-birth-to (d,y,t) x=y)

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

5

Syntax of FOL [1]

? Non-logical expressions: ? Individual constants: IC ? n-place predicate symbols: RCn (n 0)

? Individual variables: IV ? Terms: T = IVIC ? Atomic formulas:

? R(t1,...,tn) for R RCn, if t1, ..., tn T ? s=t for s, t T

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

6

3

Syntax of FOL [2]

? FOL formulas: The smallest set For such that: ? All atomic formulas are in For ? If A, B are in For, then so are ? A, (AB), (AB), (AB),(AB) ? If x is an individual variable and A is in For, then xA and xA are in For.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

7

Dolphins in FOL

Dolphins are mammals, not fish. d (dolphin(d)mammal(d) ?fish(d))

Dolphins live in pods. d (dolphin(d) x (pod(p) live-in (d,p))

Dolphins give birth to one baby at a time. d (dolphin(d) x y t (give-birth-to (d,x,t) give-birth-to (d,y,t) x=y)

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

8

4

Semantics of FOL [1]

? Model structures for FOL: M = ? U (or UM) is a non-empty universe (domain of individuals) ? V (or VM) is an interpretation function, which assigns individuals (UM) to individual constants and n-ary relations between individuals (UMn) to n-place predicate symbols.

? Assignment function for variables g: IV UM

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

9

Semantics of FOL [2]

? Interpretation of terms (with respect to a model structure M and a variable assignment g): [[]] M,g = VM(), if is an individual constant [[]] M,g = g(), if is a variable

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

10

5

Semantics of FOL [3]

? Interpretation of formulas (with respect to model structure M and variable assignment g):

[[R(t1, ..., tn)]]M,g = 1 iff

[[s=t]]M,g = 1

iff

[[t1]] M,g, ..., [[tn]] M,g VM(R) [[s]] M,g = [[t]] M,g

[[?]]M,g = 1

iff

[[]]M,g = 0

[[ ]]M,g = 1

iff

[[]]M,g = 1 and [[]]M,g = 1

[[ ]]M,g = 1

iff

[[]]M,g = 1 or [[]]M,g = 1

[[ ]]M,g = 1

iff

[[]]M,g = 0 or [[]]M,g = 1

[[ ]]M,g = 1

iff

[[]]M,g = [[]]M,g

[[x]]M,g = 1

iff

there is aUM such that [[]]M,g[x/a] = 1

[[x]]M,g = 1

iff

for all aUM : [[]] M,g[x/a] = 1

? g[x/a] is the variable assignment which is identical with g except that it

assigns the individual a to the variable x.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

11

Semantics of FOL [4]

? Formula A is true in the model structure M iff [[A]]M,g = 1 for every variable assignment g. This works best if A has no free variables.

? A model structure M satisfies a set of formulas (or: M is a model of ) iff every formula A is true in M.

? A is valid iff A is true in all model structures. ? A is satisfiable iff there is a model structure that makes it true. ? A is unsatisfiable iff there is no model structure that makes it true. ? A is contingent iff it it is satisfiable but not valid.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

12

6

Entailment and Deduction

? A set of formulas entails formula A ( |= A) iff A is true in every model of .

? A (sound and complete) calculus for FOL allows us to prove A from iff |= A by manipulating the formulas syntactically. There are many calculi for FOL: resolution, tableaux, natural deduction, ...

? Calculi can be implemented to obtain: ? theorem provers: check entailment, validity, and unsatisfiability ? model builders: check satisfiability, compute models ? model checkers: determine whether model satisfies formula ? find off-the-shelf implementations on the Internet

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

13

Two levels of interpretation

? Semantic interpretation of a NL expression in a logical framework is a two-step process: ? The NL expression is assigned a semantic representation ? The semantic representation is truth-conditionally interpreted.

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

14

7

The expressive power of FOL [1] John is a blond criminal

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

15

The expressive power of FOL [1]

John is a blond criminal criminal(j) blond(j)

Semantic Theory 2006 ? M. Pinkal/A.Koller UdS Computerlinguistik

16

8

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download