|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.