REDLOG -- Computer Algebra Meets Computer Logic
Date: July 19th (Friday)
Time: 14:00-14:20
Abstract
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.
