By using our ability to eliminate redundant constraints,
we can verify formulas of the form
.
Here,
represents a set of integer variables,
and
and
represent conjunctions of linear constraints over
.
We check to see if the constraints of
are
redundant, given that the constraints of
are true.
We can combine this capability with our ability
to eliminate existentially quantified variables to verify
more complicated formulas such as
.