Instantiating a universal whose variable does not appear in the formula results in an error
Opened this issue · 1 comments
connorjayr commented
The following decomposition in a truth tree results in an error:
forall x forall y P(y)
forall y P(y)
This is because the code does not know to what constant the user is trying to assign x
. If the variable does not appear in the formula, the assignment code should assume an arbitrary value (which will necessarily be valid since the constant will not appear in the resulting formula).
jputlock commented
This fix does not introduce that new constant to the universe, but prevents crashing when running into this scenario.