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.