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.