cyclist
cyclist copied to clipboard
ngorogiannis
Effect of Bug fix (sha 425b80) on While Abducer
I've discovered that the bug in fix in commit 425b80 affects the search carried out by the abducer and results in one of the benchmarks no longer being proved.
The benchmark in question is 11-btree-insertion.wl.
What happens is that simplification steps can now be performed after symbolic execution.
The two attached files are the debug outputs of the while abducer on this example in this commit and two commits prior, respectively.
whl_abd-425b80-11-btree-insertion-dbg.txt whl_abd-38e0af-11-btree-insertion-dbg.txt
Hi Reuben, thanks for putting this into an issue. I've been aware of this, though I suspect the proof found previously was unsound. I haven't had time to investigate though.
Hi Nikos,
No worries.
I came across it when I was re-running the benchmark suite after updating the abducer during my merge. I didn't want to spend further time investigating at this point, so that's why I put it in an issue.
When I've finished my merge (I only have Gadi's two TL tools to do now), I'm going to close the other open issue too, since I'm as confident as I can be that my work on the SL prover treats existential variables "correctly" now - specifically, it doesn't make assumptions about freshness of existential variables across the left- and right-hand sides of sequents, and introduces existentials on the right-hand side during backlinking whenever necessary. The code itself if fairly hairy, but when you're Sl_v2 is rolled out this should all get much simpler (hopefully!).
R
On 24/10/16 11:04, ngorogiannis wrote:
Hi Reuben, thanks for putting this into an issue. I've been aware of this, though I suspect the proof found previously was unsound. I haven't had time to investigate though.
— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ngorogiannis/cyclist/issues/4#issuecomment-255699751, or mute the thread https://github.com/notifications/unsubscribe-auth/AHzZPD1TTQ-OxrP_p9uRH_M8NkHPBEQJks5q3IK1gaJpZM4Kd6tj.