Transcript PPT - Universität des Saarlandes

Computational Semantics
http://www.coli.uni-sb.de/cl/projects/milca/esslli/
Day 5: Inference
Aljoscha Burchardt,
Alexander Koller,
Stephan Walter,
Universität des Saarlandes,
Saarbrücken, Germany
ESSLLI 2004, Nancy, France
Where are we by now?
So far:
Sentence:
John loves Mary.
lexicon
Linguistic Analysis…
Syntax
Semantic
construction
Why???
Why meaning?
Why logic?
Formula:
love(john, mary)
Motivations
Why meaning?
1. The big question in the background of semantics: How
do linguistic expressions relate to the world?
2. The need for inference in a broad sense is omnipresent in
linguistic processing: Getting some piece of information
out of another. This process is meaning based.
Why logic?
Using logic helps us in answering both problems at once.
Peter loves Mary and she
Meaning based linguistic
doesn't love him.
one is happy if he isn't loved
InferencesNo
by the one he loves.
• Answering questions:
A: "Is Peter happy"

Peter is not happy
B: "No"
• Discourse
„There is my car. The roof is red.“
=> The roof of this particular car.
• Pragmatics
A: „Shall we watch Athens?“, B: „Oh, I hate Sports“
 Answer is "no."
• ...
Logical Inferences
• Argumentation: Classical field => Answering questions
„Every human is mortal“, „Socrates is a human“
=> Socrates is mortal.
x.human(x) -> mortal(x), human(soc) |= mortal(soc)
• Discourse, Pragmatics, ... Inference problems during
processing:
– logical relations between readings (equivalence, implication,
contradiction)
yx.love(x,y)

xy.love(x,y)
xy.love(x,y)

yx.love(x,y)
– discourse maxims: utterance consistent? informative?…
– "lexical" inference: "Brussels lowers taxes"
– presuppositions
Next…
How do linguistic expressions relate to the world?
Building logical representations is a step towards a
scientific theory of this relation!
They're a way of replacing something we don't
understand by something we understand (at least
better).
Why? Because we have a formal way of saying what
they mean: Models.
The big question of semantics
John loves Mary and Peter doesn't.
Semantic construction
love(john,mary) love(peter,mary)
???
"Understanding language"
Logics
???
{man(john), man(peter), woman(mary),
love(john,mary)}
???

 
Cognition / Ontology
Plan for Today
• What's the advantage of FOL-formulae?
Interpretations and models
• Doing things with semantic representations
Logical Inference and Proof Theory
A calculus
• Automated Theorem Proving (first steps)
An implementation of propositional tableaux
• A sample application
FOL-semantics
What does a FO-formula mean?
• It may be true or false (that's all)
• Whether it is true or false is calculated
given a model.
So: A formula is true or false in a model.
• But what is a model?
Models
A model can be thought of as a set of basic facts that describe
a part of the world. E.g., talking about John, Mary, Peter,
love, man and woman:
–
–
–
–
–
–
–
John loves Mary.
John is a man.
Mary doesn't love John.
Peter is a man.
Mary isn't a man.
Mary is a woman.
…
In this listing:
1. Who is there?
2. Which properties do (or don't) they have?
Formally
This intuition is formalized as follows:
A model is an ordered pair of a set and a Function:
M
=
The domain:
What is there.
(D, F)
The interpretation function:
Which properties do these
things have? (and more…)
Example model
• D=
• F=
{John, Mary, Peter}
{(John, John),
(Mary, Mary),
(Peter, Peter)
(man, {John, Peter}),
(woman, {Mary}),
(love, {(John, Mary)}) }
Truth in a model
g: Assignment function, assigning values from D to variables
R(t 1,..., tn)  T
A  BMg  T
A Mg  T
g
A  BM  T
g
M
A  BMg  T
xA Mg  T
g
xA M  T
iff
iff
iff
iff
iff
iff
iff
(t  ,..., t
g
1M
A Mg  T
A Mg  F
g
A M  T
A Mg  F
A Mg '  T
A Mg '  T

g
n M
)  R
and
or
or
g
M
BMg  T
B  T
BMg  T
g
M
for some x-variant g' of g
for all x-variants g' of g
Models as Sets of Formulae
• For our purposes, models are simply sets of literals (i.e.
positive or negative atomic formulae).
 Set contains all literals that are true in the model.
• Our example:
{man(john), man(peter), woman(mary),
love(john,mary),love(mary,john),…}
• Truth of atomic formulae without variables:
R(t1,…,tn)  M
From theory to practice
• Models define the semantics of logical
languages…
• …and are an interesting concept for relating
language and the world.
• But they're also of practical importance:
They're the key to a formalization of
inference.
Now: some further important logical notions.
Inference and Entailment
• Valid inference: Truth of premises guarantees truth of
conclusion.
• Entailment: Talking about all models.
• Concept directly captures syllogistic reasoning.
P, Q, …
For all M, g such that:
and
and
PMg  T
g
QM  T
…
|=
we have:
R
RMg  T
Validity
• A related notion: Truth of a formula in all models:
Validity
g
|= A iff for all M,g: A M  T
• Validity formalizes the notion of tautology, e.g.:
Sylvester is either a cat or not.
|= cat(s) v  cat(s)
• Relation to entailment via the deduction theorem:
A |= B iff |= AB
Where are we now?
•
•
•
•
Why meaning? 
Why logic? 
Relation to the world: Models 
Inferences: Entailment and validity 
• How to compute with these notions?
How to work with all models?
Entailment and validity are both defined with
respect to all models.
Problem: There are infinitely many models.
How can we work with these notions then?
Idea: Tell whether a formula is valid or not
just by looking at it!
The answer: A calculus.
Calculi
• Calculi are rule-based systems for
manipulating formulae according to their
structure.
• Some of the resulting configurations are
called proofs.
• Formulas with proofs are called theorems.
• A good calculus produces a proof iff its input
formula is valid.
"Good" Calculi
Good Calculi are:
1. Sound: Only valid formulae get a proof.
2. Complete: All valid formulae get a proof.
In other words: All and only theorems are
valid.
|- ≡ |=
To achieve this, one has to give the right rules.
Let's try…
Tableaux: The intuition I
Truth conditions tell us what would have to hold in a model for a given
formula, e.g.:
– A and B hold in all models for A  B
– For A  B, there are two kinds of models: Those for A and those for
B.
– …
If we go on decomposing a formulas that way, we end up with sets of literals
 models
Example: smoke(john)  ( love(mary,john)   love(john,mary))
 {smoke(john), love(john, mary)}
 {smoke(john), love(mary, john)}
Tableaux: The intuition II
We know: If a formula is valid, it's always
true.
I.e.: No model makes it false.
Making formulae false:
"sign"
(smoke(john)  walk(john))F
 {smoke(john), walk(john)}

(smoke(john)  smoke(john)) F
 {smoke(john), smoke(john)}

Tableaux
If we want to know whether a formula is valid, we
systematically try to find a model that would make
it false…
… hoping that we find none.
That is, all attempts should lead to contradictions.
Next: A look at:
( ((pq) (pq)) )F
A simple fragment
Next: The rules for a tableaux calculus for
predicate logic without variables and
quantifiers.
–
–
–
–
Actually propositional logic
Advantage 1: Decidable
Advantage 2: Rules are easy
Disadvantage: Boring and restricted
More is possible – but not here and now.
Preprocessing
•
Reduce the number of connectives by
translating  and  to  and .
•
Use logical equivalences:
1. A  B   (A  B) „De Morgan“
2. A  B   (A  B)
Tableaux Inference Rules
“Mary loves Bill or John loves Mary'' |= ``John loves Mary“ ???
Summing up
• Using predicate logic as representation language
seemed to be a design decision on Monday.
• Now we're happy we did it:
– Models tell us when sentences are true.
– Models give us a concept of logical inference.
– This concept can be mechanized by calculi.
• After the break: Calculi can be implemented in
provers. And provers are useful!
More logics - Changing the language
and/or the semantics.
• Different phenomena, different logics:
–
–
–
–
Intensional logic (John seeks a unicorn)
Temporal logics (tense)
Dynamic logics (anaphora)
Higher Order (quantifiers)
• Different tasks – different tools
– Decidability and complexity
– From propositional over first order to higher order
– In between. E.g. Description logics.