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)

Solved Forms for Path Ordering Constraints. - Robert Nieuwenhuis; José Miguel Rivero (RTA, 1999)

Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. - Robert Nieuwenhuis; José Miguel Rivero (Inf. Comput., 2002)