Deduction: Automated Logic

In this paper, we describe KoMeT, a theorem prover for full first order logic. KoMeT is based on the connection method. Our main goal is to develop an adequate proof procedure by integrating a variety of different proof techniques.