In automated theorem proving, it is common to regard clauses as multisets of literals. This seems a little odd, since X or X = X so that using sets would seem to be equivalent, but both easier and more efficient.
Are there any situations where treating clauses as sets of literals gives the wrong answer despite the apparent logical equivalence so that it is actually necessary to use multisets?
At least part of the answer is to do with subsumption. The subsumption criterion commonly used is 'there exists a variable substitution that makes C a submultiset of D'. If you replace that with 'subset' then while that is still logically correct as far as it goes, a clause can subsume its own factors, which will break a calculus that uses explicit factoring.