Aussagenlogische Resolution

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

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

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

folgendes Inferenzsystem heißt Resolution:

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

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