|
Proving Implications by Algebraic ApproximationMichael Codish and Grigory Mashevitzky
Journal of Theoretical Computer Science;
165 : 57-74,
1996
Abstract:This paper applies techniques of algebraic approximation to provide effective 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 lattice. We show that the validity of a universally quantified implication psi over a possibly infinite domain can be determined by examining its validity over a simpler domain the size of which is related to the number of constants in psi. Both the known as well as the new results have high potential in providing practical automated techniques in various areas of application in computer science.Available: bibtex entry compressed postscript Related sites: Abstract from the publisher PDF from Scirus - scientific search engine Michael Codish The Department of Computer Science Ben-Gurion University of the Negev PoB 653, Beer-Sheva, 84105, Israel mcodish@cs.bgu.ac.il
|