Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interesting example of blast looping in 2016-1

view this post on Zulip Email Gateway (Aug 22 2022 at 15:02):

From: Rafal Kolanski <xs@xaph.net>
Hello,

When updating one of our branches to 2016-1 I came across blast looping
on this subgoal when it did not do so previously:

∀j∈set w. ¬ j ⟹ True ∉ set w

Interestingly, blast is OK with this one:

∀j∈set w. ¬ j = True ⟹ True ∉ set w

and also

∀j∈set w. j = False ⟹ True ∉ set w

Any ideas what changed to cause this? In this case I switched over to
fastforce due to being in a hurry, but it would be useful to understand
for future reference.

Sincerely,

Rafal Kolanski

view this post on Zulip Email Gateway (Aug 22 2022 at 15:02):

From: Lawrence Paulson <lp15@cam.ac.uk>
Your problem is not first-order and therefore lies outside the scope of blast. As I recall, there was a minor change connected with problems of that general sort. That particular example is unfortunate, but it is easily provable using other proof methods, including auto, fast and best.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 15:03):

From: Makarius <makarius@sketis.net>
For the historical record, bisection produces the following result.

The first bad revision is:
changeset: 63278:9a2377b96ffd
user: paulson <lp15@cam.ac.uk>
date: Fri Jun 10 13:54:50 2016 +0100
summary: Better treatment of assumptions/goals that are simply
Boolean variables. Also cosmetic changes.

Maybe there is more to say about it.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 15:04):

From: Lawrence Paulson <lp15@cam.ac.uk>
I will look into this but it may take some time.
Larry

view this post on Zulip Email Gateway (Aug 22 2022 at 15:20):

From: Lawrence Paulson <lp15@cam.ac.uk>
I have finally taken the time to look at this report more closely. The change made on 10 June 2016 causes blast to ignore goals than consist of a Boolean logical variable or its negation. Such variables typically cause uncontrolled branching, resulting in non-termination. Your example is a lucky case that worked anyway before that change. However, blast is a first-order prover, so such problems are out of scope.

Thanks for your report.

Larry Paulson

Last updated: Nov 21 2024 at 12:39 UTC