Clarification about negation in propositional logic

Question

I am a little stumped on the concept of resolution, and want to clarify that something is correct, primarily negation.

if an expression in CNF is ${x = (a \lor b) \land (\lnot a \lor \lnot b)}$

It's negation should be: ${\lnot x = (\lnot a \land \lnot b \land a \land b)}$

I got that as follows:

${\lnot x = \lnot(a \lor b) \land \lnot(\lnot a \lor \lnot b)}$

${\lnot x = (\lnot a \land \lnot b) \land (a \land b)}$

${\lnot x = (\lnot a \land \lnot b \land a \land b)}$

Is this correct, because I am using this as the basis for something in a larger assignment. Which involves something I read here: http://logic.stanford.edu/classes/cs157/2009/notes/chap05.html about halfway down the page is this example:

${\frac{(p, q)\\(\lnot p, \lnot q)}{(p, \lnot p)\\(q, \lnot q)}}$

where () denotes a cluase and the --- denotes the resolution from above to below. From my understanding, they have taken a pair of clauses above that are satisfiable, and made a pair of clauses that are valid (satisfiable under any assignment) below, have I misunderstood this?

Thanks.

Answer 1

Your initial negation is incorrect: the negation of

$${x = (a \lor b) \land (\lnot a \lor \lnot b)}$$

is

$$\begin{align*} \neg\Big((a\lor b)\land(\neg a\lor\neg b)\Big)&\equiv\neg(a\lor b)\lor\neg(\neg a\lor\neg b)\\ &\equiv(\neg a\land\neg b)\lor(a\land b)\;. \end{align*}$$

You failed to apply De Morgan’s law $\neg(p\land q)\equiv\neg p\lor\neg q$ correctly in your first step.

You can check this by informal reasoning. The original sentence $x$ says that at least one of $a$ and $b$ is true and at least one is false, so it says that exactly one of $a$ and $b$ is true. The final sentence in my derivation of the negation says that $a$ and $b$ are both false or both true, which clearly is the negation of the assertion that exactly one of them is true.

Added: The resolution

$$\begin{array}{} \{p,q\}\\ \{\neg p,\neg q\}\\ \hline \{p,\neg p\}\\ \{q,\neg q\} \end{array}$$

is just an abbreviation for a pair of resolutions,

$$\begin{array}{} \{p,q\}\\ \{\neg p,\neg q\}\\ \hline \{p,\neg p\} \end{array}$$

via elimination of $q$ and $\neg q$, and

$$\begin{array}{} \{p,q\}\\ \{\neg p,\neg q\}\\ \hline \{q,\neg q\} \end{array}$$

via elimination of $p$ and $\neg p$. It amounts to saying that from $p\lor q$ and $\neg p\lor\neg q$ you may derive either $p\lor\neg p$ or $q\lor\neg q$, which is surely true, if not very interesting!