HOL4 has a notion of persistent theory, so you could spawn many parallel sessions, each delivering a theory with one result, then create a single descendant theory, import all the parent theories, and chain your implications or inequalities there.
It also provides integer decision procedures, so the calls to INT_ARITH might possibly be directly substitute-able. Konrad. On Thu, Jan 28, 2021 at 5:07 PM D. J. Bernstein <d...@math.uic.edu> wrote: > Thanks for the references and suggestions. As a scaled-down example of > part of the time consumption, this takes 400 million CPU cycles: > > INT_ARITH `&193650890589077504 * (&2 * (y:int) + &1) > <= &47942158315484610560 * (&2 * (x:int) + &1) > + &135203236847161865141 > /\ > &0 <= &2655641718416121605914624 * (&2 * x + &1) > + &2208414543647439060992 * (&2 * y + &1) > + &6004289407548407186399935 > ==> > &0 <= &13137886070707932161376256 * (&2 * x + &1) > + &17509226798704706453504 * (x + y + &1) > + &36152178747194683600721967`;; > > Hand proof: take 6532449000950803555513091/700376017867732114912 and > 26794012414555294513937/5603008142941856919296 times the first and > second inequalities, add, and observe that you now have a stronger > version of the conclusion, offset by 1581608968911709059178093879/256. > > Changing INT_ARITH to g still takes around 100 million CPU cycles, which > makes me wonder whether there's some bottleneck in parsing or printing. > > The code that I wrote to do a bunch of searching to find and print the > whole sequence of relevant presumed theorems is, with no optimization > effort, thousands of times faster than this. Of course that code doesn't > have to bother with the symbolic aspects of proof manipulation. > > ---Dan > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
