Documentation

The Heuristic data type indicates the order in which variables are forgotten.

For example,

>>> vars (p ∧ q → p)
["p","q"]

( frequency ps vs ) is the list of variables vs sorted by frequency of occurrence in ps. For example:

>>> [x1,x2] = map var ["x1","x2"] :: [PolF2]
>>> frequency (S.fromList [x1,x2,x1+1]) [x1,x2]
[x2,x1]

( revFreq ps vs ) is the list of variables vs ordered in reverse order of frequency in ps. For example:

>>> [x1,x2] = map var ["x1","x2"] :: [PolF2]
>>> revFreq (S.fromList [x1,x2,x1+1]) [x1,x2]
[x1,x2]