{\sc redlog} is a system for computing with first-order logic and
propositional logic with quantification. It is tightly integrated into the
computer algebra system {\sc reduce}. Assuming a broad audience, we
motivate the use of first-order logic to model problems. Then, by
employing quantifier elimination methods, simplification techniques
and normal form computations, highly non-trivial problems can be
solved. We give an overview of {\sc redlog}'s capabilities, features
and applications. Finally we explain how computer algebra benefits
from computer logic and vice versa.