1
$\begingroup$

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).

Thank you in advance.

$\endgroup$

1 Answer 1

1
$\begingroup$

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$.

Indeed, you can think of resolution as an algorithm searching through every possible proof tree.

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – chris765
    Jan 23, 2022 at 9:47
  • $\begingroup$ 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)... $\endgroup$
    – chris765
    Jan 23, 2022 at 9:47
  • $\begingroup$ 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. $\endgroup$
    – Couchy
    Jan 23, 2022 at 19:06
  • $\begingroup$ There are some other proof finding procedures, but resolution is the only one guaranteed to find a proof if it exists (that is complete and sound) (as far as I know). $\endgroup$
    – Couchy
    Jan 23, 2022 at 19:07
  • $\begingroup$ In theory you could take any deduction system and try every possible proof tree, the problem with that is that not every proof system satisfies the subterm property which is the key property you need to do proof search (otherwise you would need to search infinitely many proof trees). Also there is actually the sequent calculus which is complete, sound, and satisfies the subterm property. $\endgroup$
    – Couchy
    Jan 23, 2022 at 19:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .