Re: [isabelle] Documentation on the simplifier



At the Isabelle Developers Workshop in 2009
(http://tphols.in.tum.de/idw.html), Stefan Berghofer described the
basics of how one would go about (re)implementing the simplifier.

It's not a description of the theory, but the Isabelle theory file
(http://tphols.in.tum.de/IDW/Conversions.thy) provides a nice
description of conversionals and they can be composed to build up
something like the simplifier.

For some theory about rewriting, I like "Term Rewriting and All That" by
Baarder and Nipkow.

best,
lucas

Steve W wrote:
> Hi all,
> 
> Does anyone know if there's any documentation on how the simplifier works?
> It'd be good if it covers both the theoretical and implementation aspects.
> I've tried tracing the ML code, but there are quite a few functions involved
> and they aren't documented unfortunately.
> 
> Thanks,
> Steve
> 

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.