[isabelle-dev] Experiments in best-first-search rewriter
nipkow at in.tum.de
Sun Nov 2 20:50:45 CET 2014
There is an awful lot of literature on rewriting which you may want to look at.
A good starting point is the practically unbeatable equational prover
Waldmeister http://www.waldmeister.org/ which is also available via
sledgehammer. It uses something called unfailing completion, which is an
efficient semidecision procedure for equational logic. Why do I mention
Waldmeister? Because it should do the (purely equational) job when simp fails.
Of course there is something to be said for a more lightweight tool than
Waldmeister, eg something like your rewriter. It certainly does happen that simp
goes into a loop, although we have learned to prove around such situations.
Moreover, BFS could be a very costly way of avoiding loops. Note also that I am
not aware of any other prover that comes with a built-in BFS rewriter. This
could indicate that in practice BFS is not that useful after all.
This may sound very negative, but I would merely suggest to establish that there
is a market for your approach before investing significant time on it.
On 02/11/2014 16:56, Bohua Zhan wrote:
> Hi, everyone
> My name is Bohua Zhan, a postdoc in mathematics at MIT. I am
> interested in doing some experiments in automated proof techniques in
> Isabelle. I have been reading the documentations and existing code for
> some time, but this is my first attempt at writing some code, so here
> it is (attached).
> I am trying to implement a simplifier / rewriter that uses
> best-first-search instead of depth-first-search as the current simp
> tactic does. This avoids a major problem with DFS simp: being trapped
> into loops by rewriting rules that can be used back and forth or
> repeatedly. This implementation memorizes terms that have already been
> Two examples are given at the end: the first refers to the permutation
> example in section 6.4 of the new Isabelle Cookbook manual, rewriting:
> pi1 . (c, pi2 . ((rev pi1) . d)
> = (pi1 . c, pi1 . (pi2 . (rev pi1) . d))
> = (pi1 . c, (pi1 . pi2) . (pi1 . ((rev pi1) . d)))
> = (pi1 . c, (pi1 . pi2) . d)
> avoiding the use of ".aux" (which I suppose is not the ideal solution).
> The second example is simplification with ring axioms. I certainly
> don't propose this is how it should be done, but just to test how
> large an example this rewriter can handle without any domain-specific
> Any suggestions? One major feature to be added is dealing with rules
> with assumptions. I would especially like to see examples of hard
> rewriting problems that come up in actual proof development.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev