Documentation

(independenceRuleAux v p ps acum) is the union of the set accum, which ramains invariant, and the set of polynomials obtained after applying independenceRule with respect to v between polynomial p and every polynomial from set pps, including itself. However, to improve efficiency the process is terminated if a zero occurs. This is because a zero in the polynomial set is sufficient for the tool to return False.

(independenceRuleKB v pps acum) is the union of the set accum, which ramains invariant, and the set of polynomials obtained after applying deltaRule with respect to v between every polynomial from set pps. For example,

>>> [x1,x2,x3] = (map var ["x1","x2","x3"]) :: [PolF2]
>>> independenceRuleKB x1 (S.fromList [x1]) (S.fromList [1])
fromList [1]
>>> independenceRuleKB x1 (S.fromList [x1,x1*x2,x1*x3]) (S.empty)
fromList [x2x3,x2,x3,1]

(forgetVarKB v ps) is the set of polynomials obtained after applying to ps the independence rule with respect to v. For example, >>> x1 = (var "x1") :: PolF2 >>> x2 = (var "x2") :: PolF2 >>> forgetVarKB x2 (S.fromList [x2,x1*x2,x1+1]) fromList [x1,x1+1,1] >>> forgetVarKB x1 (S.fromList [x1,x1+1,1]) fromList [0]

For example,

>>> saturateKB (S.fromList[1],[]) monomialOrd
True
>>> x1 = (var "x1") :: PolF2
>>> saturateKB (S.fromList[x1,x1+1],[x1]) monomialOrd
False