When I try it in HOL Light on my machine it takes about 0.074 seconds,
which is around 250 million CPU cycles according to the clock speed
from "lscpu". This is the same order of magnitude that Dan was seeing.
On the whole, the procedures like INT_ARITH are mostly fast enough for
everyday
Just for clarification: the HOL4 term parser handled the supplied term
without alteration, and
intLib.ARITH_CONV is the HOL4 analog of INT_ARITH.
On Thu, Jan 28, 2021 at 6:59 PM Konrad Slind wrote:
> Also, there seems to be some inefficiency: the posted formula gets proved
> quite quickly
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
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
Dan,
On Mon, 2021-01-25 at 14:40 +0100, D. J. Bernstein wrote:
> I have another newbie question regarding HOL Light; again happy to
> hear about other HOL variants if those have easier answers.
Since you mentioned other HOL variants, I would like to point out that
Isabelle can take advantage of
Hi Dan,
So, in a nutshell, you've got N proof scripts in HOL Light that you want
to fit together as one coherent proof in a single session, but that
would take far too much processing to do so in practice. So you want to
execute these in N parallel HOL Light sessions, recording the
I have another newbie question regarding HOL Light; again happy to hear
about other HOL variants if those have easier answers.
I'm in the typical post-human-proof situation where a program found a
"proof" that's too tedious for a human to verify (in the conventional
sense, not PCPs). For
