Fixed: Formula::Exists::Rectify() didn't register variables.
The bug implied that Ex x P(x) v Ex Q(x) would be normalized to Ex x Ex x (P(x) v Q(x)) because Rectify(Ex x P(x)) did not register the variable x and consequentially Rectify(Ex x Q(x)) didn't know it was registered already. Also removed the wrong assertion that in Formula::Bel::FreeVars() that alpha and (~alpha v beta) must have the same free variables.
Loading
Please register or sign in to comment