For a question statement given in the book "A Concise Introduction to Logic" by Patrick J. Hurley, I want to derive the FOL resolution proof tree using the method of contradiction.
The Question statement is
If all the physicians are either hematologists or neurologists, then there are no cardiologists. But Dr. Frank is a cardiologist. Therefore, some physicians are not neurologists. (P, H, N, C)
Using the predicate interpretations of the above statements given in this website, I have converted them to Conjunctive Normal Form (CNF) clauses as follows to build up the proof tree.
all the physicians are either hematologists or neurologists, then there are no cardiologists.
1 : P(A) ∨ ￢C(z)
2 : ￢H(A) ∨ C(z)
3 : ￢N(A) ∨ C(z)
Dr. Frank is a cardiologist
4 : C(Frank)
Negation of Conclusion "some physicians are not neurologists"
5: ￢P(x) ∨ N(x)
My issue is, from which two statements should we 1st use to draw the proof tree? Statement 1 with 5, or 3 with 5, or 4 with 1 or ....? Do we need to consider the order of the statements in the KB?
This can be written as $\forall p (Hp\lor Np)\to (\lnot\exists q Cq)$
This can be written as $Cf$.
This can be written as $\exists r \lnot Nr$.
This is assuming cardiologists are physicians.
To prove the last statement from the other two, compute the tableau of $$\lnot((\forall p (Hp\lor Np)\to (\lnot\exists q Cq))\land Cf)\to (\exists r \lnot Nr)$$ and show that it is closed.
You should get something like this:
Each path ends in a contradiction, hence the result.