The decision procedure is based on the algorithm used in cvc4, which is itself based on the omega test.

this package provides a library for the haskell programming language, compiled for profiling. see http://www.haskell.org/ for more information on haskell.