I'm trying to use resolution to prove that:

$\forall x(A(x) \lor B(x)) \land \neg B(a) \models A(a)$

My attempt was to try resolve $\neg B(a)$ and $B(x)$ by forcing the substitution of x for a. This gives

$\forall aA(a) \models A(a)$ which is true.

Is this correct? I am unsure as I am still trying to understand resolution in predicate logic.

Thanks for any help!


To do resolution, you need to negate the conclusion, put that into clauses, add that to the clauses from the premises, and then derive the empty clause.

Thus, you get the clause $\{\neg A(a) \}$ from the negation of the conclusion, and clauses $\{ A(x), B(x) \}$ and $\{ \neg B(a) \}$ from the premises.

Now you can resolve the latter two clauses by setting $x=a$, resulting in the clause $\{ A(a) \}$.

And that clause resolves with the $\{ \neg A(a) \}$ clause, resulting in the empty clause $\{ \}$

That ends the resolution, but to explain why that proves the argument to be valid: the empty represents a contradiction, and so what you have shown is that if you assume th conclusion is not true, you get a contradiction which, by Proof by Contradiction, shows that the conclusion has to be true given the turht of the premises ... meaning the argument is valid.


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.