基于Robinson Resolution Principle：如何将resolvent转换为goal clause？

Great question—let’s break this down clearly, since the relationship between resolvents (from Robinson’s general resolution) and goal clauses (in SLD resolution) can feel tricky at first, especially when your professor frames goal clauses as resolvents.

First, let’s ground ourselves in the core connection: In SLD resolution, every new goal clause you generate is exactly a Robinson resolvent—just rephrased in query syntax. Here’s a step-by-step way to convert between the two:

Step 1: Recall the syntax mappings #

First, remember how goal clauses and program clauses translate to the standard clausal form used in Robinson resolution:

• An SLD goal clause like ?- A₁, A₂, ..., Aₙ. corresponds to the clausal form ¬A₁ ∨ ¬A₂ ∨ ... ∨ ¬Aₙ (a disjunction of negative literals).
• An SLD program clause like A ← B₁, B₂, ..., Bₖ. corresponds to A ∨ ¬B₁ ∨ ¬B₂ ∨ ... ∨ ¬Bₖ (a disjunction with one positive literal and any number of negative literals).

Step 2: Compute the Robinson resolvent #

Suppose you have:

• Current goal clause G: ?- A₁, A₂, ..., Aᵢ, ..., Aₙ. (clausal form: ¬A₁ ∨ ... ∨ ¬Aᵢ ∨ ... ∨ ¬Aₙ)
• A program clause C that unifies with Aᵢ: A ← B₁, ..., Bₖ. (clausal form: A ∨ ¬B₁ ∨ ... ∨ ¬Bₖ)
• A most general unifier (mgu) θ that makes Aᵢθ = Aθ.

To compute the Robinson resolvent:

1. Apply θ to both clauses.
2. Remove the complementary literals (¬Aᵢθ from G’s clausal form, Aθ from C’s clausal form).
3. Combine the remaining literals into a single disjunction:

   (¬A₁ ∨ ... ∨ ¬Aᵢ₋₁ ∨ ¬Aᵢ₊₁ ∨ ... ∨ ¬Aₙ ∨ ¬B₁ ∨ ... ∨ ¬Bₖ)θ
   

Step 3: Convert the resolvent to an SLD goal clause #

This is the straightforward part—you just reverse the clausal form to query syntax:

• Take every negative literal ¬P in the resolvent and turn it into a positive literal P.
• Replace the disjunction (∨) operators with commas (,, which represent conjunction in goal clauses).
• Prepend the ?- query marker.

Example Walkthrough #

Let’s make this concrete with an example:

1. Current goal: ?- p(X), q(X). (clausal form: ¬p(X) ∨ ¬q(X))
2. Program clause: p(a) ← r(a). (clausal form: p(a) ∨ ¬r(a))
3. mgu θ: {X/a} (unifies p(X) and p(a))

Compute the resolvent:

• Apply θ to both clauses: ¬p(a) ∨ ¬q(a) and p(a) ∨ ¬r(a)
• Remove complementary literals ¬p(a) and p(a)
• Resolvent clausal form: ¬q(a) ∨ ¬r(a)

Convert to goal clause:

• Turn ¬q(a) into q(a), ¬r(a) into r(a)
• Replace ∨ with commas: q(a), r(a)
• Add ?-: ?- q(a), r(a).

Key Takeaway #

Your professor’s framing is spot-on: SLD goal clauses are resolvents in disguise. The conversion is just a syntax shift—Robinson’s resolvent uses clausal form (disjunction of negatives), while SLD goal clauses use query form (conjunction of positives) because it’s more intuitive for expressing subgoals we want to prove.

内容的提问来源于stack exchange，提问作者Qwerto