An Implementation Kernel for Theorem Proving with Equality Clauses. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (APPIA-GULP-PRODE, 1996)

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (CADE, 1997)

Barcelona. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (J. Autom. Reason., 1997)