1
$\begingroup$

We know that a resolution derivative of a clause $C$ from a set of clauses $\mathcal{C}$ is a sequence $(C_1, ..., C_n)$, so that:

  1. $C_n = C$ and
  2. for all $1 \leq i \leq n$ the following holds: $C_i \in \mathcal{C}$ or there is $j,k < i$ with $C_i \in \text{Res}(C_j,C_k)$.

If this holds, then $C$ is a resolution proof from $\mathcal{C}$ and is written as $\mathcal{C} \vdash_R C$. However, a resolution rebuttal of a set of clauses $\mathcal{C}$ is a resolution derivative of the empty clause $\square$.

I understand the part with the $\square$ because there is an example to illustrate it. However, I am honestly lost about the entire first section. What is happening here? I need to understand that section so that I can understand resolution calculus, so any help is appreciated.

PS - this is translated from German and I'm not sure if some of the terms translate well in English. So if there is anything wrong, please mention it in the comments.

$\endgroup$
2
  • $\begingroup$ English: "Rebuttal" = refutation, "derivative" = derivation. Which "first part" do yo mean -- the 1., 2. part or the "If this holds" part? Also, do you have a link to the source you can provide us so we can better address the specific formulation on your textbook? -- Notation and terminology can vary between different presentations. $\endgroup$
    – lemontree
    Dec 5, 2020 at 4:11
  • $\begingroup$ I think the way "resolution proof" is used here is just another name for the derivation, and a resolution refutation is a special such derivation with $C = \Box$. $\endgroup$
    – lemontree
    Dec 5, 2020 at 4:23

1 Answer 1

0
$\begingroup$

Let $a, b, d, a', \cdots$ be propositional variables. Let $A, D$ be disjuncts of literals. Let $W1$ and $W2$ be conjuncts of disjuncts of literals within a complete wff.

In some resolution proof settings, each clause is a disjunction of literals. A literal is either a propositional variable by itself or a negated propositional variable.

I'm going to answer a slightly different question than the one you posed ... at least initially. I will assume that there is some prefix of clauses $C_1, \cdots , C_w$ that are independent of each other and constitute the premises of the proof $\mathcal{C}$. In the question that you posed, only $C_1$ is the only clause that is not a product of a resolution step. I'll address this problem a little bit later.

If we have two clauses such that the left clause has a positive literal and the right clause has the corresponding negative literal, then we can infer a new clause that is formed by joining the remaining literals from both the left and right clauses.

a \/ a' \/ b       !b \/ d \/ d'
--------------------------------
        a \/ a' \/ d \/ d'

Let $A$ and $D$ be metavariables ... standing in for arbitrary disjunctions of literals.

A \/ b     !b \/ D
------------------
      A \/ D

This inference rule is valid if only if $(A \lor b) \land (\lnot b \lor D) \implies A \lor D$ is an unconditional tautology. We can convince ourselves that this is true using truth tables.

The turnstile symbol $\vdash$, possibly with subscripts, is often used to denote that the thing on the right hand side is a syntactic consequence of the things on the left hand side. It can also be used to denote that a proof of some sort exists given some premises.

In the cases I've seen, $\vdash$ is frequently used to represent an inductively defined predicate on two sets of well-formed formulas. That seems to be the case here, $\mathcal{C}$ is both an ordered list of premises and a proof.


The fact that $C_1$ is the only unconstrained clause in the list makes me think that in the presentation in your book, $C_1$ is not restricted to being a disjunction of literals.

We can deal with this problem by insisting that $C_1$ is in conjunctive normal form, i.e. it is a conjunction of disjunctions of literals.

In this case, we can modify our inference rule slightly by ignoring all but one conjunct in each of the input clauses. Let $W1$ and $W2$ each stand for an arbitrary number of ignored conjuncts in each of our premises

W1 /\ (A \/ b)     (!b \/ D) /\ W2
----------------------------------
            (A \/ D)

Because of the semantics of and, we can treat $W1$ and $W2$ the same way we treat the other clauses that aren't being used as premises.

Also, we can do the following with both conjuncts being taken from the same clause. We're forced to do this for $C_2$.

   (A \/ b) /\ W1 /\ (!b \/ D)
----------------------------------
            (A \/ D)

If we set up the inference rule this way, there are very strong limits on what $\mathcal{C}$ can end in (it must end with a disjunction of literals). I don't know whether this is acceptable.

Also, note that $\vdash_R$ is an inductive relation.

$ J \vdash_R K $ is true if and only if there's a resolution step sending two conjuncts of $J$ to $K$

$ \Gamma, J \vdash_R K $ is true if and only if there's a resolution step sending some conjuncts in $ \Gamma \cup \{J\}$ to $K$ and $\Gamma \vdash_R J$.

$\endgroup$
0

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.