# Re: [isabelle] Automatic heuristic simplifier setup

Till Mossakowski schrieb:

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.

`Certainly nothing automated. And I would even have a hard time
``describing my intuition.
`

A related question is: which kinds of loops are automatically
detected by the simplifier already?

`The loop test works on a rule by rule basis. Given P ==> l = r it
``rejects this orientation of the rule if
`
- there are extra variables in r not in l or P, or
- the head of l is a variable, or
- l occurs in r or P, or
- P is empty and l matches r, or
- l is a constant but r is not
If the opposite orientation also fails, P ==> (l=r) = True is added.

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.

`There is no such work. I suspect that trying to prove termination is
``extremely hard and Isabelle specific. Detecting loops on the other hand
``may be valuable, in particular for novices.
`
Tobias

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