Abstract: Up to now we have seen various ways to construct logical formulae as meaning representations for sentences. But we don't yet know what to do further with such formulae. We will now learn how to do useful work with meaning representations like the ones we saw being constructed in the last lectures.If we utter a sentence, we transport information. One way of exploiting this information is to find out what follows from the sentence. The parallel task on the level of meaning representations is that of ↗inference from the formula for that sentence. So it would be a great step forward if we could automate the process of drawing inferences from such formulae. For this purpose, one uses calculi known from theoretical logic. The method that we will discuss in this chapter at length is that of semantic tableaux. We start by discussing inference for a propositional logic (» The Logic PLNQ), leaving the more complex issue of first order inference for later. In the next chapter, we will see that the Prolog implementation of propositional tableaux is straightforward.
Table of Contents
What is Inference, and how do we use it in Computational Semantics? Knowing what follows from a sentence is an indispensable ingredient of understanding it. Correspondingly, finding out what can be inferred from the formula constructed for a sentence is a very important task in computational semantics. Here are some of the reasons why this is so:
Often, we can only fully understand a sentence by inferring from it (together with our background knowledge). For example if we ask someone whether he has already listened to the latest record of Carla Bley, he may answer Oh, I hate Jazz!. To understand this as an answer to our question, we have to infer that he in fact has not listened to the record (maybe due to his musical half-heartedness).
Inference from a sentence may be necessary to react properly to it, e.g. to answer a question.
Already in the process of meaning construction itself, inference may help us reduce the number of readings that can be constructed. This may greatly reduce the load for subsequent processing stages.
A limited amount of inference may even be essential to any language understanding: Given a complex sentence (resp. a complex formula for it), we have to infer which basic atomic facts have to hold for the sentence to be true. This sort of inference is known as model generation and we will come back to it at some length in » [Sidetrack] Model Generation.
Up to now, we've only seen definitions that capture the notion of logical consequence (see » Valid Arguments) semantically. In this section, we will develop a method to get a grip on this notion operationally: We will see how we can use syntactic calculi to actually compute what follows from a formula. But let us proceed step by step.
Tableaux Calculi We have discussed semantic construction methods at some length in earlier chapters. So according to the diagram we've seen just above (» o5077), the next thing we need in order to really do natural language semantics is an appropriate calculus. As we promised, we will not use the somewhat unintuitive and clumsy Hilbert-style calculus (» A simple Logical System: Propositional Logic with Hilbert-Calculus) for any practical purposes. Instead, in this section we will introduce a so-called tableaux calculus (first only for propositional logics, later we will extend it to first order logic). Before we come to the formal characterization of our tableaux calculus, we will give you a more intuitive introduction.
Tableaux Web-Interface In the next chapter, we will discuss the implementation of our propositional tableaux calculus just presented. If you want to use the calculus right away, have a look at our Web-Interface. You can either generate tableaux for some given example formulae or type in formulae yourself (using our familiar Prolog syntax). This might help you doing your exercises.
Add annotations to the nodes of the tableaux above. The annotations should indicate from where each node resulted, and why. For example, node 1 would be annotated "from Input", and node 2 something like "from 1, making a conjunction true". Additionally, the closure nodes (⊥) should be annotated with the numbers of the respective contradictory nodes.
[You have to read the sidetrack on derived inference rules (» Sidetrack: Practical Enhancements for Tableaux) to do this exercise.] To see the value of the derived inference rules, prove or refute the formula (p⇔q)⇔(q⇔p).
In » The Maxim of Quality we claim that the utterance Mary doesn't like Mutz is inconsistent with the discourse If Mutz is a Siamese cat, then Mary likes her. Mutz is a Siamese cat. because we can construct a closed tableaux for the formula: (¬(SIAMESECAT(MUTZ)⇒LIKE(MARY,MUTZ))∧SIAMESECAT(MUTZ)∧¬LIKE(MARY,MUTZ))F resp. the equivalent: (¬(¬(SIAMESECAT(MUTZ)∧¬LIKE(MARY,MUTZ)))∧SIAMESECAT(MUTZ)∧¬LIKE(MARY,MUTZ))F Construct this tableaux.
Then construct the tableaux needed to check whether Mary has a husband. is informative in the context If Mary is married then she has a husband. She is married. (treating the pronouns as in the example above).