Aussagenlogische Resolution

Formel (A∨¬B∨¬C)∧(C∨D) mathend000# in konjunktiver Normalform

dargestellt als {{A,¬B,¬C},{C, D}} mathend000#

(Formel = mathend000# Menge von Klauseln, Klausel = mathend000# Menge von Literalen, Literal = mathend000# Variable oder negierte Variable)

folgendes Inferenzsystem heißt Resolution:

• Axiome: Klauselmenge einer Formel,
• Regel:
  • Prämissen: Klauseln K₁, K₂ mathend000# mit v∈K₁,¬v∈K₂ mathend000#
  • Konklusion: (K₁ $\setminus$ {v})∪(K₂ $\setminus$ {¬v}) mathend000#

Eigenschaft (Korrektheit): wenn $${\frac{{K_1,K_2}}{{K}}}$$ mathend000#, dann K₁∧K₂→K mathend000#.