context:
given two formula phi and psi, we may have situation such as (x + a) vs (y + y) which are not equivalent, but (x + a) vs (b + y) which are equivalent. free variable symbols are not important but free variable positions is.
the method is_syntaxically_equivalent and is_masked_formula_equivalent are currently directional, assuming we compare the second formula with the first that may contain free variables. but the second formula as well may contain free variables. in the implementation of minimal logic (m0), this bug is blocking the derivation of the theory based on axiom schemas.
notes:
syntaxical equality would require that the variables be the same objects.
syntaxical equivalence takes free variables into account.
[ ] review the logic of the formula syntaxical equivalence methods, properly accounting for free variables in both formula
[ ] implement an extensive series of test including:
context: given two formula phi and psi, we may have situation such as (x + a) vs (y + y) which are not equivalent, but (x + a) vs (b + y) which are equivalent. free variable symbols are not important but free variable positions is.
the method is_syntaxically_equivalent and is_masked_formula_equivalent are currently directional, assuming we compare the second formula with the first that may contain free variables. but the second formula as well may contain free variables. in the implementation of minimal logic (m0), this bug is blocking the derivation of the theory based on axiom schemas.
notes: syntaxical equality would require that the variables be the same objects. syntaxical equivalence takes free variables into account.