0
$\begingroup$

I'm kind of desperate at this point about this question.

A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ such that each $C_i$ is either a clause of $F$ (possibly with the variables renamed) or follows by a resolution step from two preceding clauses $C_j ,C_k$, with $j, k < i$. We write $\operatorname{Res}^*(F)$ for the set of clauses $C$ such that there is a derivation of $C$ from $F$.

The question is to give an example of a finite set of clauses $F$ in first-order logic such that $\operatorname{Res}^*(F)$ is infinite.

Any help would be appreciated!

| cite | improve this question | |
$\endgroup$
  • $\begingroup$ I have never heard of variable renaming in the context of Resolution. Perhaps you meant reordering? $\endgroup$ – Yuval Filmus May 23 at 15:59
  • $\begingroup$ It seems that your task is impossible. A finite set of clauses involves finitely many variables, and there are finitely many clauses over these variables. $\endgroup$ – Yuval Filmus May 23 at 15:59
  • $\begingroup$ Perhaps you're using some very odd definition of Resolution. $\endgroup$ – Yuval Filmus May 23 at 16:00
  • 1
    $\begingroup$ @RnHdw Can you provide a reference from where you got this question (if there is one)? $\endgroup$ – prime_hit May 23 at 18:39
  • $\begingroup$ Big Hint: Since resolution is a complete rule of inference, the question is equivalent to asking if there is any finite set of axioms with an infinite number of consequences. What comes to mind? We can help lead you to it. $\endgroup$ – ShyPerson May 25 at 4:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.