Resolution allows to generate new clauses for an existing set of clauses.In many cases, the rule is simple:{ a, b }     { -a, b }----------------------        { b }But what if the clauses contain multiple literals suitable for resolution?{ a, b }     { -a, -b }-----------------------        { ? }If we choose a, then the result should be { b, -b } by definition. Is this correct?If it is, what does this imply? I would assume { b, -b } to always be true as it means $b \lor \lnot b$ which is a tautology. Is this correct, and if it is not, what else does the result imply?
Resolution with multiple variables
logic;propositional logic