\begin{center}
\LARGE
REDLOG -- Computer Algebra Meets Computer Logic 

\end{center}

\begin{center}
\Large
Andreas Dolzmann, Thomas Sturm

\end{center}

\noindent
Date:  July 19th (Friday)\\
Time:  14:00-14:20\\

\begin{center}
\large
Abstract
\end{center}

REDLOG is a package that extends the computer algebra system reduce to a computer logic
system, i.e., a system that provides algorithms for the symbolic manipulation of first-order
formulas over some temporarily fixed language and theory. In contrast to theorem provers, the
methods applied know about the underlying algebraic theory and make use of it. Though the focus
is on simplification, parametric linear optimization, and quantifier elimination, REDLOG is
designed as a general-purpose system. It has been applied successfully for solving non-academic
problems, mainly for the simulation of networks. We describe the functionality of REDLOG as it
appears to the user, and explain the design issues and implementation techniques. 

