Bug with existential quantifier decomposition

Question

Bug with existential quantifier decomposition

Closed this issue a year ago · 5 comments

See tree below. The existential decomposition rule should decompose Ex P(x) either into P(b) (classic rule), or branch into two branches: one with P(a), and the other with P(b) (his is the alternative rule that in some cases can avoid infinite trees). However, as you can see the P(a) is being allowed in the main branch rather than have its separate branch (I added the A v B so I could put P(b) in a branch)

Answer 1 · 2023-02-28T19:37:52.000Z

I think I've identified the bug. I will attempt the fix later tonight and do some testing. Hopefully we can get a fix pushed to live by tomorrow.

Answer 2 · 2023-02-28T19:50:25.000Z

Cool! Thanks Jeff!

Answer 3 · 2023-02-28T21:44:06.000Z

And just to be sure: below is a correct use of the alternative existential rule

Answer 4 · 2023-03-01T04:59:13.000Z

Update: this is going to take some more investigation but I'm actively working on it.

Answer 5 · 2023-03-24T00:15:51.000Z

@Bram28 I believe this fix resolves the issue but I'm going to keep deliberating and testing since it's such a simple change. I've redeployed the service so the fix is now live on the site.