Resolution

• ein Resolutions-Schritt:
  $${\frac{{(x_1 \vee \ldots \vee x_m \vee y), (\neg y \vee z_1 \vee \ldots \vee z_n)}}{{x_1 \vee \ldots \vee x_m \vee z_1 \vee \ldots \vee z_n}}}$$

• Sprechweise: Klauseln C₁, C₂ werden nach y resolviert.
• Schreibweise: C = C₁⊕_yC₂
• Beispiel:
  $${\frac{{x\vee y,y\vee \neg z}}{{x\vee\neg z}}}$$

• Satz: {C₁, C₂} $\models$ C₁⊕_yC₂. (Die Resolvente folgt aus den Prämissen.)