Here I will discuss first-order logic and the various methods for its semi-automation (tableaux, inverse method, resolution, model elimination), as well as some methods for equational reasoning. This was one of the primary interests in the 1970s and it still an active field today.