(Redirected from Redlog)
Jump to: navigation, search

Authors: Andreas Dolzmann and Thomas Sturm

REDLOG provides an extension of the computer algebra system REDUCE to a computer logic system. The name stands for REDUCE logic system.

REDLOG implements symbolic algorithms on first-order formulas with respect to user-chosen first-order languages and theories. The available domains include real numbers, integers, combination of reals with integers, complex numbers, p-adic numbers, quantified propositional calculus, term algebras, queues.

Redlog originated from the implementation of real quantifier elimination.

External Links