Disprover: Free identifiers in the proof are not handled correctly
Description
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
Details
Assignee
Sebastian Krings
Sebastian KringsReporter
Daniel Plagge
Daniel PlaggePriority
More fields
Story Points, Original estimate
More fields
Story Points, Original estimateCreated January 27, 2014 at 9:10 AM
Updated January 27, 2014 at 9:57 AM
Resolved January 27, 2014 at 9:57 AM
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.