Ganzinger, Harald Programming Logics, MPI for Informatics, Max Planck Society;
https://rdcu.be/dwBMb (Publisher version)
Ganzinger, H. (1996). Saturation-based Theorem Proving: Past Successes and Future Potential. In M. A. McRobbie, & J. K. Slaney (Eds.), Automated Deduction - Cade-13 (pp. 1-1). Berlin: Springer.