In the normal operation of the Omega test, we eliminate any constraint
that is made redundant by any other single constraint
(e.g., is
made redundant by
).
Upon request, we can use more aggressive techniques to eliminate
redundant constraints. We use incomplete tests that can flag a constraint
as definitely redundant or definitely not redundant, and a backup
complete test. This capability is used when verifying implications
and simplifying formulas involving negation.