PROVING IMPLICATIONS BY ALGEBRAIC-APPROXIMATION

This paper applies techniques of algebraic approximation to provide ef fective algorithms to determine the validity of universally quantified implications over lattice structures. We generalize the known result which states that any semilattice is approximated in the two element l attice. We show that the validity of a universally quantified implicat ion psi over a possibly infinite domain can be determined by examining its validity over a simpler domain the size of which is related to th e number of constants in psi. Both the known as well as the new result s have high potential in providing practical automated techniques in v arious areas of application in computer science.