Previous | 
Home
Section: New Software and Platforms
The Redlog Computer Logic System
Functional Description
Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on first-order formulas.
Redlog generally works with interpreted first-order logic in contrast to free first-order logic. Each first-order formula in Redlog must exclusively contain atoms from one particular Redlog-supported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlog-supported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT, and many more.
In 2016 there was significant progress with the generation of models for real satisfiability problems [15]. When obtained via quantifier elimination by virtual substitutions, such models contain in general non-standard numbers like positive infinitesimal and infinite values. In an efficient post-processing step Redlog now generates standard models.