Prove propositional logic by resolution.

Question

Prove $$[(p→q) \wedge (qr→s)]\to [pr→s],$$ which is the same as $$[(\lnot p\lor q) \wedge (\lnot (qr) \lor s)]\to [\lnot (pr) \lor s]$$

I believe it can just be done with algebra rules, but I got stuck at the end.

And this is not a programming question.

Thanks.

Answer 1

We do not have $(\overline{p}\lor q)\wedge (\overline{q\wedge r}\lor s)\equiv \overline{p\wedge r}\lor s$. $\,\text{RHS}\equiv \overline{p}\lor \overline{r}\lor s$.

Assume $s$. Then $\text{RHS}$ is true, but $\text{LHS}\equiv \overline{p}\lor q$, which is not necessarily true.

But we do have $(\overline{p}\lor q)\wedge (\overline{q\wedge r}\lor s)\to\overline{p}\lor \overline{r}\lor s$. I assume that's what you wanted to say - please be more clear next time.

$$\overline{p}\lor \overline{r}\lor s\lor \overline{(\overline{p}\lor q)\wedge (\overline{q\wedge r}\lor s)}$$

$$\stackrel{\text{DeMorg}}\equiv \overline{p}\lor \overline{r}\lor s\lor (p\wedge\overline{q})\lor (q\wedge r\wedge \overline{s})$$

$$\stackrel{\text{Distr}}\equiv p\lor \overline{q}\lor \overline{r}\lor s\lor (q\wedge r\wedge \overline{s})$$

$$\stackrel{\text{Distr}}\equiv p\lor \overline{q}\lor \overline{r}\lor [(s\lor (q\wedge r))\wedge (s\lor \overline{s})]$$

$$\equiv p\lor \overline{q}\lor \overline{r}\lor s\lor (q\wedge r)$$

$$\stackrel{\text{Distr}}\equiv p\lor \overline{r}\lor s\lor \overline{q}\lor r\equiv T\lor p\lor s\lor \overline{q}\equiv T$$

Or simply by observation:

We must have $(\overline{p}\lor q)$. If $\overline{p}$, we're done. Otherwise $q\wedge(\overline{q\wedge r}\lor s)$, which is

$$q\wedge (\overline{q}\lor \overline{r}\lor s)\stackrel{\text{Distr}}\equiv (q\wedge\overline{q})\lor (q\wedge (\overline{r}\lor s))\equiv q\wedge (\overline{r}\lor s),$$

so we must have $\overline{r}\lor s$. If $\overline{r}$, we're done. If $s$, we're done. Or do it like Berci said in the comments.

Answer 2

If it's proof by resolution you need, rewrite the premises to $\neg p\vee q$ and $\neg q\vee\neg r\vee s$, then apply resolution on $q$: $$\begin{array}{ccc} \neg p\vee q & & \neg q\vee\neg r\vee s \\ \hline & \neg p \vee \neg r \vee s \end{array}$$ Then rewrite that conclusion to $p\wedge r\to s$.