[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
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 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