Engel, Thorsten Programming Logics, MPI for Informatics, Max Planck Society;
Engel, T. (1996). Quantifier Elimination in Second-Order Predicate Logic. Master Thesis, Universität des Saarlandes, Saarbrücken.