Hustadt, Ullrich Programming Logics, MPI for Informatics, Max Planck Society;
Hustadt, U. (1999). Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD Thesis, Universität des Saarlandes, Saarbrücken.