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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
