[isabelle] Automatic heuristic simplifier setup

Is there a general heuristic (perhaps even implemented) what should
be put into the Isabelle simplifier?  Of course, this cannot replace
manual adpations; however, it could at least provide a good
starting point.
A related question is: which kinds of loops are automatically
detected by the simplifier already?
Is there work on using termination proof tools in this
context? Probably, commutativity rules would need to be
excluded when fedding a termination checker, because Isabelle
can handle them.

Similar questions apply to the classical reasoner.

Till Mossakowski

Till Mossakowski      Cartesium, room 2.051  Phone +49-421-218-64226
DFKI Lab Bremen                              Fax +49-421-218-9864226
Safe & Secure Cognitive Systems             Till.Mossakowski at dfki.de
Enrique-Schmidt-Str. 5, D-28359 Bremen   http://www.dfki.de/sks/till

Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313

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