Logik-Basierte Sprachverarbeitung WS22/23 - Summary

A model for NLU

1. speech processing: acoustic signal → word hypothesis graph
   
2. syntactic processing: word sequence → phrase structure
   
3. semantics construction: phrase structure → (quasi-)logical form
   
4. semantic pragmatic analysis: (quasi-)logical form → knowledge representation
   
5. problem solving: using the generated knowledge
   

Everyone is here.

Radical Semantic View

The sentence literally means that everyone in the world is here, so is generally false. An interpreter recognizes that the speaker said something false.

Radical Pragmatic View

The semantics are incomplete and what the sentence means is determined by the context of utterance and speaker's intentions.

Intermediate View

The quantifier "every" contains a slot for information which is contributed by the context. Extralinguistic information is required to fix the meaning.

Proposition

A proposition is a sentence about the actual world or a class of worlds deemed possible whose meaning can be expressed as being true or false

Belief

A belief is a proposition that an agent holds true about a class of worlds

Knowledge

knowledge is justified, true belief (summarist's objection: Gettier Problem)

Observation

Given a world \(w\), the observed value of a proposition \(\varphi\) can be determined by observations. An observer is an agent that perceives \(\varphi\) is as true in \(w\). An observation is reproducible, iff it can be observed by different observers in different situations.

Phenomenon

A phenomenom is a proposition that is reproducibly observable to be true in a class of worlds.

Explanation

A proposition \(\psi\) follows from a proposition \(\varphi\), iff \(\psi\) is true in any worlds where \(\varphi\) is. An explanation of a phenomenom \(\varphi\) is a set \(\Phi\) of propositions, such that \(\varphi\) follows from \(\Phi\).

Counterexample

A world \(w\) is a counterexample to a proposition \(\varphi\), if \(\varphi\) is observably false in \(w\). A proposition is falsifiable, iff counterexamples are theoretically possible and feasibly observable.

Hypothesis

A hypothesis is a proposed explanation of a phenomenom that is falsifiable.

Foundational Meaning Theory

A meaning theory that tries to explain why language expressions have the meaning they have in terms of mental states of individuals and groups

A natural language fragment is the language of a context-free grammar

abstract Grammar = {
    cat
        Name;     -- proper name ("Ethel", ...)
        TransVerb;
        InTransVerb;
        VP;
        S;
        Conn;    -- connectives like "and", "or", ...
        NP;   -- noun phrases
        Noun;
        Det;    -- determiner ("the", "every", "a", ...)

    fun
        makeVP : TransVerb -> NP -> VP;
        makeVP2 : InTransVerb -> VP;
        makeS : NP -> VP -> S;
        negateVP : VP -> VP;

        makeNP : Det -> Noun -> NP;  -- "the" -> "cat" -> "the cat"
        makeNP2 : Name -> NP;        -- "Peter" -> "Peter"

        -- "howl" -> "scream" -> "howl and scream"
        combineVP : VP -> Conn -> VP -> VP;
        combineS : S -> Conn -> S -> S;

        and : Conn;
        or : Conn;

        the : Det;
        every : Det;
        some : Det;

        cat_ : Noun;
        dog: Noun;
        teacher: Noun;
        peter : Name;
        mary : Name;
        fido : Name;
        love : TransVerb;
        poison : TransVerb;
        sleep : InTransVerb;
        laugh : InTransVerb;
}

concrete GrammarEng of Grammar = {
    lincat
        Name = Str;
        TransVerb = {fin: Str; inf: Str};
        InTransVerb = {fin: Str; inf: Str};
        VP = {fin: Str; inf: Str};
        S = Str;
        ReflexiveVerb = Str;
        Conn = Str;
        NP = Str;
        Noun = Str;
        Det = Str;

    lin
        dog = "dog";
        cat_ = "cat";
        teacher = "teacher";
        peter = "Peter";
        mary = "Mary";
        fido = "Fido";
        love = {fin="loves"; inf="love"};
        poison = {fin="poisons"; inf="poison"};
        sleep = {fin="sleeps"; inf="sleep"};
        laugh = {fin="laughs"; inf="laugh"};

        and = "and";
        or = "or";
        the = "the";
        every = "every";
        some = "a" | "some";

        makeNP determiner noun = determiner ++ noun;
        makeNP2 name = name;

        combineVP v1 c v2 = {
          fin=v1.fin++c++v2.fin;
          inf=v1.inf++c++v2.inf
          };
        combineS s1 c s2 = s1 ++ c ++ s2;
        negateVP vp = {
          fin="doesn't" ++ vp.inf;
          inf="not" ++ vp.inf
          };

        makeVP verb name = {
          inf=verb.inf ++ name;
          fin=verb.fin ++ name
          };
        makeVP2 verb = {fin=verb.fin; inf=verb.inf};

        makeS name vp = name ++ vp.fin;
}

Soundness

A calculus \(C\) is sound, iff \(\mathcal{H} \vDash A\) whenever \(\mathcal{H} \vdash_C A\)

Completeness

A calculus \(C\) is complete, iff \(\mathcal{H} \vdash_C A\) whenever \(\mathcal{H} \vDash A\)

Deduction Theorem

A calculus \(C\) obeys the deduction theorem if
\[ \mathcal{H}, A \vdash_C B \text{ iff } \mathcal{H} \vdash_C A \implies B \]

Entailment Theorem

A Logic obeys the entailment theorem if
\[ \mathcal{H}, A \vDash B \text{ iff } \mathcal{H} \vDash A \implies B \]

theory plnq_proofs : ur:?LF =
    include ?plnq ❙

    ded : o ⟶ type ❘ # ⊢ 1 prec 5 ❙

    andEl : {A:o} {B:o} ⊢ A ∧ B ⟶ ⊢ A ❘ # aEl 3 ❙
    andEr : {A:o} {B:o} ⊢ A ∧ B ⟶ ⊢ B ❘ # aEr 3 ❙
    andI  : {A:o} {B:o} ⊢ A ⟶ ⊢ B ⟶ ⊢ A ∧ B ❘ # aI 3 4 ❙

    orIl  : {A:o} {B:o} ⊢ A ⟶ ⊢ A ∨ B ❙
    orIr  : {A:o} {B:o} ⊢ B ⟶ ⊢ A ∨ B ❙
    orE   : {A:o} {B:o} {C:o}
          ⊢ A ∨ B ⟶ (⊢ A ⟶ ⊢ C) ⟶ (⊢ B ⟶ ⊢ C) ⟶ ⊢ C ❙

    implE : {A:o} {B:o} ⊢ A ⟶ ⊢ A ⇒ B ⟶ ⊢ B ❙
    implI : {A:o} {B:o} (⊢ A ⟶ ⊢ B) ⟶ ⊢ A ⇒ B ❘
          # ⇒I 3 ❙
❚

kind o type.
type neg o -> o.
type and o -> o -> o.
type or o -> o -> o.

kind iota type.
type mary iota.
type john iota.
type love iota -> iota -> o.

type atomic o -> prop.
atomic (neg _A)    :- !, fail.
atomic (and _A _B) :- !, fail.
atomic (or _A _B)  :- !, fail.
atomic _A.

kind mo type.
type markF o -> mo.
type markT o -> mo.

type member mo -> (list mo) -> prop.
member X [X|_].
member X [_|Xs] :- member X Xs.

type tableau (list mo) -> (list mo) -> prop.
tableau [markT (and A B)|T] M :- tableau [markT A, markT B | T] M.
tableau [markF (and A _B)|T] M :- tableau [markF A | T] M.
tableau [markF (and _A B)|T] M :- tableau [markF B | T] M.
tableau [markT (neg A)|T] M :- tableau [markF A | T] M.
tableau [markF (neg A)|T] M :- tableau [markT A | T] M.
tableau [markF A |T] [markF A |M] :-
    atomic A, tableau T M, not (member (markT A) M).
tableau [markT A |T] [markT A |M] :-
    atomic A, tableau T M, not (member (markF A) M).
tableau [] [].

theory fol_proofs : ur:?LF =
    include ?plnq_proofs ❙
    include ?fol ❙

    forallE : {B : ι ⟶ o} {C : ι} ⊢ ∀ B ⟶ ⊢ B C ❙
    existsI : {B : ι ⟶ o} {C : ι} ⊢ B C ⟶ ⊢ ∃ B ❙
    forallI : {B : ι ⟶ o} ({X : ι} ⊢ B X) ⟶ ⊢ ∀ B ❙
    existsE : {B : ι ⟶ o} {C : o} ⊢ ∃ B ⟶ ({w : ι} ⊢ B w ⟶ ⊢ C) ⟶ ⊢ C ❙

    equalI : {A : ι} ⊢ A ≐ A ❙
    equalE : {A : ι} {B : ι} {P : ι ⟶ o} ⊢ A ≐ B ⟶ ⊢ P A ⟶ ⊢ P B ❙

    description_axiom : {S : ι ⟶ o} {a : ι}
            ⊢ ((S a ∧ ∃! S) ⇔ (the S) ≐ a) ❙
❚

α-equivalence

\((\lambda x.\, A) =_{\alpha} (\lambda y.\, [y/x]A)\)

β-reduction

\((\lambda x.\, A) B =_{\beta} [B/x]A\)

η-reduction

\((\lambda x.\, A x) =_{\eta} A\) , iff \(x\) is not free in \(A\)

We want to encode quantifiers in the lambda calculus with \(\Pi\) and \(\Sigma\) types.
If we interpret objects of type \(\iota \to o\) as sets, we can define:

\begin{align*} (\forall x_{\alpha}.\, A) &:= \Pi_{\alpha} (\lambda x_{\alpha}. A)\\ (\exists x_{\alpha}.\, A) &:= \Sigma_{\alpha} (\lambda x_{\alpha}. A) \end{align*}

"The" cannot be treated with regular quantifiers.

John killed the cat in a bathroom with a hammer.

To allow modifiers on verbs we extend the argument structure of action verbs with an event argument.
\[ \exists e.\, \exists x,y.\, \mathrm{bathroom}(x) \land \mathrm{hammer}(y) \land \mathrm{kill}(e, \text{peter}, \iota\, \text{cat}) \land \mathrm{in}(e,x) \land \mathrm{with}(e,y) \]

Take apart davidsonian predicates further, add event participants via thematic roles.

John killed the cat with a hammer

\[ \exists e.\, \exists x.\, \mathrm{hammer}(x) \land \mathrm{killing}(e) \land \mathrm{agent}(e,\text{peter}) \land \mathrm{patient}(e, \iota\, \text{cat}) \land \mathrm{with}(e,x) \]
As a neo-davidsonian system can get by without functions and only unary and binary predicates, model generation is easier.

Some modifiers are incompatible with some events.

event type	example
state	know the answer, stand in the corner
process	run, eat apples
accomplishments	run a mile, eat an apple
achievements	reach the summit

Deal with dynamic phenomena by replacing existential quantifiers.

Discourse

A discourse is a sequence of sentences.

Discourse Representation Theory (DRT)

A logical system which uses discourse referents to model quantification and pronouns.

Discourse Representation Structures (DRS)

A DRT formula that introduces a set of discourse referents and specifies their meaning via conditions.

A student owns a book.

\(X,Y\)
\(\mathrm{student}(X)\)
\(\mathrm{book}(Y)\)
\(\mathrm{own}(X,Y)\)

If a farmer owns a donkey, he beats it.

\(X,Y\)	\(\Longrightarrow\)
\(\mathrm{farmer}(X)\)		\(\mathrm{beat}(X,Y)\)
\(\mathrm{donkey}(Y)\)
\(\mathrm{own}(X,Y)\)