[isabelle-dev] Experiments in best-first-search rewriter

[Tobias Nipkow]

Hi Bohua,

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.

Best
Tobias

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
> explored.
>
> 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
> knowledge.
>
> 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.
>
> Thanks,
> Bohua
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141102/e0167a4e/attachment.bin>