$(30$ points$)$ Provide a formal proof that the resolution inference algorithm is a sound and complete inference

method. More formally, we are given a knowledge base $KB$ represented in conjunctive normal form $($and "AND

of ORs"$),$ and a query $,$ whose negation is also given in CNF form $($i$.$e$.$ it is another "AND of ORs"$).$

$($a$)(10$ points$)$ Prove that resolution in propositional logic is sound.

$($b$)(20$ points$)$ Prove that resolution in propositional logic is complete, assuming that the query $$ is a single

binary variable. You need to show that if applying the resolution algorithm to $K{B}^{{?}^{?}}$not$$ results in an empty

resolvent then $KB|==.$ You may assume that the knowledge base $KB$ is internally consistent, i$.$e$.$ it does

not contain any contradictory statements, or statements that resolve to an empty resolvent ${?}_{|}{?}_{?}.$ Intuitively, it is

the addition of not$$ that "causes" the empty resolvent.

$($c$)($bonus points$)$ Prove that resolution in propositional logic is complete for an arbitrary query $.$