On Fri, 6 May 2011 15:22:25 -0700 (PDT)
tvn nguyenthanh...@gmail.com wrote:
given a list of equality expressions, is there a way to remove all the
members that can be inferred by others in the list so that the final
list contains only independent expressions and they imply all the ones
that
Hi, actually I do use Qepcad and other smt solvers like Z3/ CVC3 etc for
non-linear inequalities and linear inequalities. Basically I use them to
see if the conjunction of e1,...,e_n imply e_n+1 , if it does then I can
remove e_n+1. However this is also not the right approach for finding
given a list of equality expressions, is there a way to remove all the
members that can be inferred by others in the list so that the final
list contains only independent expressions and they imply all the ones
that were removed.
For example
[x == 2, x^2 = 4] = [x == 2]
