This chapter introduces into various aspects and methods of the formalization and automation of processes involved in performing inferences. It views automated inferencing as a machine-oriented simulation of human reasoning. In this sense classical deductive methods for first-order logic like resolution and the connection method are introduced as a derived form of natural deduction. The wide range of phenomena known as non-monotonic reasoning is represented by a spectrum of technical approaches ranging from the closed-world assumption for data bases to the various forms of circumscription. Meta-reasoning is treated as a particularly important technique for modeling many significant features of reasoning including self-reference. Various techniques of reasoning about uncertainty are presented that have become particularly important in knowledge-based systems applications. Many other methods and techniques (like reasoning with time involved) could only briefly — if at all — be mentioned.