Redlog—Computing with Logic

What is Redlog?

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 has been publicly available since 1995 and is constantly being improved. The name Redlog stands for Reduce Logic System.

Interpreted First-Order Logic

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.

Quantifier Elimination Procedures

Effective quantifier elimination procedures for the various supported theories establish an important class of methods available in Redlog: Given a first-order formula \(\varphi\), Redlog computes an equivalent formula \(\varphi′\) that does not contain any quantifier. As an example in nonlinear real arithmetic consider the following input formula: \[\varphi = \forall x \exists y (x^2 + xy + b > 0 \land x + ay^2 + b \leq 0).\] For this input Redlog computes \(\varphi′ = a < 0 \land b > 0.\)

Decision Methods

For the theories supported by Redlog, quantifier elimination procedures are in particular decision procedures. For instance, reusing the above \(\varphi\) and calling quantifier elimination on \(\forall a \exists b (\varphi)\) Redlog computes "false."

Besides these quantifier elimination-based decision methods there are specialized, and partly incomplete, decision methods, which are tailored to input from particular fields of application.

Connectivity

Reduce has been designed as an interactive computer algebra system. The Reduce source distribution includes a C library for managing Reduce processes and communicating with these processes.

Using this C library, the communication language can be quite easily and flexibly adapted. Besides communication via Reduce command strings, an XML-based communication protocol can be easily realized. In an ongoing project, a subset of the SMTLIB v2.0 language is being realized in order to qualify Redlog as an SMT theory solver.

License

Both Reduce and Redlog are open-source and freely distributed under a very liberal FreeBSD License.