# Testing entailment via resolution calculus technique confusion

Given a knowledge base $$KB$$ and a formula $$\varphi$$ in propositional logic. One of the ways of testing entailment i.e. proving $$KB \models \varphi$$ is using resolution calculus.

My confusion: I don't see the need of using resolution calculus for proving entailment, when -according to my observation- we can instead use the same technique used with resolution calculus for testing entailment with just "any sound (correct) calculus" (doesn't have to be complete nor refutation complete).

To recap the idea of using resolution for testing entailment and showcase where my real question lies:

To show $$KB \models \varphi$$, we reduce the problem of general entailement to unsatisfiability via the contradiction theorem i.e. $$KB \models \varphi \quad \Longleftrightarrow \quad KB \cup \{\neg \varphi\} \models \bot.$$ So, now the goal is to show$$\quad KB \cup \{\neg \varphi\} \models \bot.$$
And we can do so by showing $$KB \cup \{\neg \varphi\} \vdash_{\textbf{R}} \bot$$, where R is the resolution calculus and if we do so, we would have proved $$KB \models \varphi$$.

My issue is in the second step, if we show $$KB \cup \{\neg \varphi\} \vdash_{\textbf{R}} \bot$$, then this implies $$KB \cup \{\neg \varphi\} \models \bot$$ (proving $$KB \models \varphi$$ via contradiction theorem), but this implication is only true since R is sound and R being refutation complete has nothing to do with it, right? Hence my question what's the need of resolution calculus , when we can just replace it with any sound system. I know it has just one rule and other systems might not (but this is still not a satisfactory answer for me).

Recall a calculus $$\mathbf{C}$$ is called $$\textit{refutation-complete}$$ if for every knowledge base $$KB$$ $$KB \models \bot \quad \Longrightarrow \quad KB \vdash_{\textbf{C}} \bot.$$

And we know that resolution calculus is refutation complete and sound (correct).

For a logical system to be complete means that if there exists a proof, then it is provable in your system. In the case of resolution, completeness means the resolution algorithm is guaranteed to find a proof of $$KB\cup\{\phi\}\vdash_R \bot$$ given $$KB\cup\{\phi\}\vDash\bot$$.
• Sorry, but I'm not sure how this answers my question still. The goal is still to show $KB \cup \{\varphi\} \models \bot$, so it is not yet given. What it is the advantage of doing that with resolution than any other say complete sound system? Whether we do so with resolution or any other sound system, if we show $KB\cup\{\varphi\}\vdash \bot$, then we have shown $KB\cup\{\varphi\}\vDash\bot$, which is what we want. Jan 23, 2022 at 9:47
• And if the system is resolution or any other complete one, then we should be able to go through every possible proof tree and if we show it is not provable, then it is not true that $KB \models \varphi$... So don't see why resolution has an advantage over other systems except that it has one rule (and it could be that there are other refutation complete sound systems with one rule but that I don't know)... Jan 23, 2022 at 9:47
• The goal is actually to show $KB\cup\{\phi\}\vdash \bot$ (note $\vdash$ rather than $\vDash$). That is to show that $\bot$ is derivable rather than modelable or "true". Completeness means given something has a model, there exists a proof in this system. All you should care about is that the goal you are trying to prove is actually true before trying to derive a proof of it. Jan 23, 2022 at 19:06