We have discussed semantic construction methods at some length in earlier chapters. So according to the diagram we've seen just above, 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 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.