Verify Implications

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 .

Web Accessibility