Hi! 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?
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. Thanks! Vlad ------------------------------------------------------------------------- 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
