A Unification graph with constraints for intelligent backtracking in deduction systems. - Dilger, Werner (Fachbereich Informatik, Univ. Kaiserslautern. Interner Bericht, 1984)