1
$\begingroup$

In resolution can I use two inferred clauses to reach the empty set?

Consider this set of clauses: $\{ p \lor q,\neg p \lor r, \neg p \lor \neg r, p \lor \neg q\}$

\begin{align*} \quad p \lor q\quad &|\quad p \lor \neg q \ \rightarrow \quad p \\ \quad p \quad &|\quad \neg p \lor r \ \rightarrow \ \quad r \\ \quad \neg p \lor \neg r\quad &|\quad r \quad \ \rightarrow \quad \neg p \\ \quad \neg p \quad &|\quad p \ \rightarrow \quad \varnothing \end{align*}

In this case I infered both $\neg p$ and $p$, can I use resolution on them? Or can I only resolve with the given clauses?

I'm also a bit confused on why I can't infer the empty clause from: $\{p \lor q, \neg p \lor \neg q \}$

$\endgroup$
3
$\begingroup$

"In this case I infered both ¬p and p, can I use resolution on them? "

Yes, you can.

"I'm also a bit confused on why I can't infer the empty clause from: {p∨q,¬p∨¬q}"

Resolution, in propositional logic, is the disjunction of all literals except those two literals which complement each other, and thus resolve into the rest of the formula. With (p∨q) and (¬p∨¬q) you can resolve to (q∨¬q) (cancelling p) or (p∨¬p). Either way though you get a tautology. This is the exact opposite of resolving to the empty set. Thus, if you could infer to the empty clause, you could get a different truth value than what resolution can actually yield in such a case.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.