Re: [Hol-info] HOL Light set comprehensions

Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC? I would think that GSPEC would have to choose a fresh variable, and I've never understood how that's to be done, because you have know that your new fresh variable hasn't already been chosen. So I would think that t

[Hol-info] Deadline extended: FLOPS 2014 call for papers

** NEWS: Submission deadline extended. - Title, abstract, and draft paper by December 13, 2013 - Full paper by December 15, 2013 (23:59 anywhere in the world) **

[Hol-info] How to define Double integral

I just want to define a Double integral like "integral (c,d)(\y. integral(a, b)(\x. f x * y))" this define just can do on HOL4, but can't compute the internal integral,because the \x. belong to from negative infinity to positive infinity,but the variable of internal integral just belong to (a,b). S

[Hol-info] Classical Logic and Computation 2014 in Wien - First Call for Papers

-- -- First Call for Papers -- ---

[Hol-info] Call for papers: Nonlinear Reasoning

Special Issue—Journal of Automated Reasoning NONLINEAR REASONING A variety of mature techniques for analyzing systems of linear inequalities have been imported to the domain of automated reasoning. In contrast, techniques for nonlinear functions are still being developed and examined. Nonlinea