QuMuLab / python-nnf

Manipulate NNF (Negation Normal Form) logical sentences
https://python-nnf.readthedocs.io
ISC License
17 stars 9 forks source link

Fix up comparisons with disperate variable sets #11

Open haz opened 4 years ago

haz commented 4 years ago

When a theory doesn't mention all of the variables, then counting, comparing, etc all become incorrect. Ultimately, a fix will need to come in the form of an NNF potentially storing a superset of the variables currently mentioned in descendants via the walk functionality.

haz commented 4 years ago

This assumption should go away once this issue is resolved.

blyxxyz commented 4 years ago

I gave this some thought during initial development but didn't come up with anything that really felt right.

One fix could be to add an optional keyword argument names for passing an explicit set of variables.

Comparing using the current behavior of .equivalent() is resistant to this problem, at least.

haz commented 4 years ago

Ya, I considered the names argument too. Problem there is that it proliferates -- many places might need it (or have sub-procedures that need it). The make_smooth operation is certainly one that would require it...