On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > RESOLUTION IS STATED AS: > > ((p v q) ^ (!p v r)) -> (q v r) > > So you have to get > > xRr <-> !xRr > p = xRr > !p = xRr > > ??? > > Mind you, only 1 inference rule is needed, modus ponens
Resolution is also complete as an "only needed" inference rule, but these things are not complete in the way you think. If you are using MP as your only inference rule then --> IS YOUR ONLY CONNECTIVE, so you have to RE-WRITE any and everything that started out using /\ , V , or <--> TO USE --> INSTEAD, IF you are going to use nothing but MP.
Similarly, since resolution ONLY operates on conjunctions of disjunctions, IF you are going to use resolution as your only inference rule, THEN you AGAIN have TO REWRITE everything that PREVIOUSLY had <--> or /\ in it AS a collection of disjunctions.
In particular (going for resolution), p <--> q becomes p --> q And q --> p; so, therefore,
--> is the wrong connective for resolution; you have to translate --> to V in order to use resolution. Since, by definition, p --> q means ~p V q, the above pair of converse conditionals become ~rRr V ~rRr and rRr V rRr . Since disjunction is idempotent, each of these two-disjunct disjunctions becomes a ONE-junct -junction (a "unit clause"), and the two things you are trying to "resolve" become
~rRr resolved with rRr. If you resolve THOSE two WITH EACH OTHER then you very quickly get THE EMPTY CLAUSE, which is a "proof of false", which proves that the original collection of disjunctions was inherently contradictory, which is exactly the result you want, since this REALLY IS a paradox.