Books on Computational Semantics by Patrick Blackburn & Johan Bos
Representation and Inference for Natural Language
A First Course in Computational Semantics
Chapter 4. Propositional Inference

Here we start examining the second major theme of the book: how to perform inferencing using the representations we now know how to build. In this chapter we take our first steps towards this goal. We discuss tableaux and resolution based proof methods for propositional calculus, and show how to implement them in Prolog. We then introduce and discuss some number of theoretical concepts (such as completeness and decidability) and relate them to the consistency and informativity checking tasks introduced in Chapter 1.