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.


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