Leven, Peter Programming Logics, MPI for Informatics, Max Planck Society;
Leven, P. (1998). Integrating Clausal Decision Procedures in a Tactic Based Theorem Prover. Master Thesis, Universität des Saarlandes, Saarbrücken.