[bitc-dev] BitC prover strategy
Jonathan S. Shapiro
shap at eros-os.org
Mon Dec 6 22:50:40 EST 2004
I have been pondering a prover strategy question. I'ld like to open it
We have been heading in the direction of building a prover, on the
grounds that Isabelle is insufficiently automated. It has occurred to me
that this may be short-sighted. Here is an alternative.
Suppose that instead of building a new prover, we create Isabelle/BitC.
This is similar to Isabelle/ISAR, except that the language of theory
expression is BitC. There is certainly no reason that we would need to
restrict ourselves to the style of recdef definitions that I can see.
On the topic of automation, we can either develop new tacticals or
modify the term rewriting engine of Isabelle to detect and blacklist
On the other hand, once we are doing this it will be true that pretty
much the *only* part of Isabelle we will be preserving is the rewriting
engine, which may not be that big a deal.
Jonathan S. Shapiro <shap at eros-os.org>
More information about the bitc-dev