Let a multivalent clause have the form ?j (xj ∈ Sj) where each xj has a finite domain Dxj and each Sj ⊂ Dxj.
Generalize the resolution algorithm to obtain a complete inference method for multivalent clauses, and prove completeness.
Define an analog of unit resolution.
Hints: a resolvent can be derived from several clauses. Resolving on xj requires taking an intersection. Multivalent resolution can be used in dynamic backtracking methods.