Resolution Principle - First Order Logic

Question

We are in First Order Logic. I have two clauses and i use the Robinson's Resolution Principle. After applying the principle, what i obtain is another clause, called resolvent.

What the resolvent represent ? What kind of info it carries ?

Answer 1

The resolvent simply represents a statement that is a logical consequence from the two original clauses.

Remember that a clause like $\{ P, Q \}$ can be seen as a disjunction $P \lor Q$. So, when you resolve clauses $\{ P, Q \}$ and $\{ \neg P, R \}$ to get the resolvent $\{ Q, R \}$, you are really inferring the claim $Q \lor R$ from the claims $P \lor Q$ and $\neg P \lor R$ ... which is indeed a valid inference.