Computing with Logic

Redlog is integrated with the interactive computer algebra system REDUCE. It supplements the open-source computer algebra system REDUCE with more than 100 functions on first-order formulas. Redlog has been publicly available since 1995 and is systematically being improved and developed further. 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 domain, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlog-supported domains include nonlinear real arithmetic (Tarski Algebra), Presburger arithmetic, parametric quantified Boolean formulas, and many more.

Symbolic Computation

Redlog provides a productive interactive environment for constructing, analyzing, and manipulating formulas. This includes various normal form computations, advanced logical and algebraic simplification techniques, and quantifier elimination and decision procedures. All this can be combined with the symbolic computation power of the host computer algebra system REDUCE.

Quantifier Elimination

Effective quantifier elimination procedures for the various supported theories play a central role in Redlog: Given a first-order formula φ, Redlog computes an equivalent formula φ' that does not contain any quantifier. The screenshot shows an example in the real domain.

Screenshot

Decision Methods

Redlog's quantifier elimination procedures are also decision procedures. For instance, Redlog's quantifier elimination computes "false" for the decision problem ∀a∃b(φ) with φ as above. Some further decision methods in Redlog are not based on quantifier elimination.

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. Besides communication via REDUCE command strings, e.g., an XML-based communication protocol can be easily realized.

License

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