We begin this chapter by defining the syntax and semantics of first-order logic (the semantic representation formalism we use in the book). We pay particular attention to the intuitions and technicalities that lie behind the satisfaction definition, a mathematically precise specification of how first-order languages are to be interpreted in models. We then introduce the three inference tasks we are interested in: the querying task, the consistency checking task, and the informativity checking task. Following this, we write a first-order model checker: this is a tool for handling the querying task. To close the chapter, we discuss the strengths and weaknesses of first-order logic as a tool for computational semantics.