Vladislavs Jahundovics wrote: > I have a question regarding Presburger arithmetics in HOL. HOL > supports decision procedures such as Omega Test and Cooper's > algorithm to decide about *closed* Presburger formulas. What if I > need to do just universal quantification of some variables in an > open formula? The question is the following: how to obtain an open > Presburger formula f(y) in HOL if we have !x.f(x,y) initially? Is it > possible at all? Or, rather, how much work and expertise is required > to do such things in HOL?
The HOL implementation of Cooper's algorithm automatically puts a universal quantification around free variables in goals. This means that the implementation automatically turns !x. f (x, y) into !y x. f (x,y) If the latter is true, then so too is the former. If the latter is false, the former may or may not also be false. You can be more sophisticated than just this in fact. For example, using its quantification maneuvering, the HOL implementation will prove f(x) < y ==> f(x) < y + 3 This is not difficult to implement, even in HOL. > In particular, I am interested in Cooper's algorithm. I have been > developing a framework for formal verification of parameterized > systems which works with Presburger formulas and uses Omega > Test. However, the size of DNFs is a huge problem, therefore I count > on Cooper's algorithm which does not require input formulas to be in > DNF. The only implementation of Cooper's algorithm I could found so > far is in HOL. There is an implementation of Cooper's algorithm in Isabelle/HOL. If you're not interested in LCF-style proof and the use of higher-order logic, and if you don't need alternating quantifiers, you might find the various SMT solvers do a good job on your problems. Michael. ------------------------------------------------------------------------- Check out the new SourceForge.net Marketplace. It's the best place to buy or sell services for just about anything Open Source. http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
