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.
To fulfill the demand for quickly locating and searching documents.
It is intelligent file search solution for home and business.
Related download
- 1 meaning and semantics
- chapter 3 describing syntax and semantics university of texas at
- the semantics of types university of new haven
- semantic theory lecture 2 type theory universität des saarlandes
- semantic types and type shifting conjunction and type umass
- semantics i id
- types of meaning in semantics
- semantics
- compositional semantics harvard university
- semantics the analysis of meaning