kror-shack
commented
1 year ago A temporary workaround fix was introduced in commit #1ccb9a2 .
Changes introduced
Temporary increase of permutations
const permutations = generatePermutations( [...usedSubstitutes], totalQuantifiers + 1 );
Conditional to make use of the permutations
if (conclusion.join("").includes(combination[i])) { continue; }
Type: Bug
Description:
It seems as though Universal Generalization does not check for allness.
This issue started occurring after commit ( #e0237dd), which introduced a way to differentiate existentially instantiated "a" as "_a" from a constant "a", such that during run time, existentially and universally instantiated constants are not differentiated apart from when generalizing so that the restriction on UG of not generalizing over an existential variable is respected. The changes do respect the restriction on universal generalization, but for the user input, it shows no way of differentiating existentially instantiations from other constants, which makes it seem that the program does not check for allness of the variables.
Note : - Allness: Generalizing all of the same variables when performing UG or EG.
Fix:
After inferring the deduction steps change Existential Instantiations to variables not yet used i.e., change every variable with an underscore behind it to a new one not yet introduced.