Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

Disprover: Free identifiers in the proof are not handled correctly

Description

When an identifier is added during a proof, it is not handled correctly by ProB. ("No counter examples found due to unfixed deferred sets")

I attach a project with the example proof. The error arises in the proof for the goal "a/={}". An identifier e is added by first adding a hypothesis "#e.e:b" and then instantiating e by clicking on the exists symbol in the hypotheses.

Environment

None

Attachments

2
  • 27 Jan 2014, 09:11 AM
  • 27 Jan 2014, 09:10 AM

Gliffy Diagrams

Activity

Show:

Daniel Plagge January 27, 2014 at 9:57 AM

You're right, I added the partition axiom later to be sure that nothing is missing, but forgot to move it to the top.

Sebastian Krings January 27, 2014 at 9:22 AM

The partition-hypothesis is the last one in the context. Hence, it can not be used to prove axm4. So there is in fact an unfixed deferred set?

I changed the order of the hypotheses so that the deferred set is fixed when working on axm4. Then, a counter-example is found.

Daniel Plagge January 27, 2014 at 9:13 AM

In the screenshot the identifier is "x" not "e" as written in the description. But in the attached project it is "e".

Cannot Reproduce

Details

Assignee

Reporter

Priority

More fields

Created January 27, 2014 at 9:10 AM
Updated January 27, 2014 at 9:57 AM
Resolved January 27, 2014 at 9:57 AM
Configure