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

  mathend000#

• Sprechweise: Klausel C mathend000# entsteht, indem Klauseln C₁, C₂ mathend000# nach nach der gemeinsamen Variablen y mathend000# resolviert werden,
• Schreibweise: C = C₁⊕_yC₂ mathend000#
• Satz: {C₁, C₂} $\models$ C₁⊕_yC₂ mathend000#.