As we learn in this chapter, full first-order inference is a lot harder than propositional inference. For a start, first-order logic is undecidable, hence there is no hope for a full algorithmic solution to the consistency and informativity checking tasks. But all is not lost. We discuss unification, and show that it can be combined with the tableaux and resolution methods to yield first-order theorem provers; sophisticated theorem provers based on unification offer a useful negative test for consistency and informativity. We then argue that modern model builders offer an interesting tool for performing positive tests for consistency and informativity, and develop a Perl script for calling theorem provers and model builders in parallel.