Email Gateway (Aug 18 2022 at 10:50): Email Gateway (Aug 18 2022 at 10:50):From: Till Mossakowski <Till.Mossakowski@dfki.de>
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
Email Gateway (Aug 18 2022 at 10:51):From: Tobias Nipkow <nipkow@in.tum.de>
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
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
Last updated: May 03 2024 at 12:27 UTC