Resolution Principle in First Order Logic

Question

Suppose that we are in First Order Logic and we have a set of clauses.

I want to prove that a certain clause is a logical consequence of this set of clauses.

Is it correct to use the Resolution Principle in this case (negating the goal clause and deducing the empty clause)?

Answer 1

Careful... What do you mean by 'negating the goal clause'? Say the goal clause is $\{ A, B \}$, what would be the negated version of that clause? You can't say it's $\neg \{ A, B \}$, that's nonsense... that's not even a clause.

And you don't want $\{ \neg A, \neg B \}$ either, since $\{ A, B \}$ corresponds to $A \lor B$, and so what you really want is $\neg A \land \neg B$, which corresponds to two clauses $\{ \neg A \}$ and $\{ \neg B \}$.

OK, but that is propositional logic. With FOL, things get a lot more hairy. For example, if the conclusion is $\forall x \ P(x)$, then putting that into a clause gives you $\{ P(x) \}$. But when you negate that, you should not get $\{ \neg P(x) \}$, for that would correspond to $\forall x \ \neg P(x)$, and what you want is of course the clause you would get for $\neg \forall x \ P(x)$, which is the clause for $\exists x \ \neg P(x)$, which is $\{ \neg P(c_0) \}$ with $c_0$ being a Skolem constant. And with multiple quantifiers, things get even more hairy, for now you may need function symbols for the Skolemization process.

So, my advice is to translate the 'goal clause' into a FOL statement, negate it, and work out the result so it can be put back into clauses. In fact, if you start with a set of FOL statements (which is what typically happens), I would definitely not take the goal statement, put into goal clause(s), and then try to negate that/those clause(s), but rather immediately negate the statement, and put that into clauses.

But yes, all these precautions set aside, you're right: If the negation of some clause $C$, when correctly put into (possibly multiple) clauses, when added to the original clause set, allows you to infer the empty clause, then that shows indeed that that clause $C$ logically follows forom the original clause set.