Waldmann, Uwe Automation of Logic, MPI for Informatics, Max Planck Society; Programming Logics, MPI for Informatics, Max Planck Society;
Waldmann, U. (2002). Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II). Journal of Symbolic Computation, 33, 831-861.