Resolution als Inferenzsystem

mehrere Schritte:

• Schreibweise: M $\vdash$ C
• Klausel C ist ableitbar aus Klauselmenge M
• Definition:
  • (Induktionsanfang) wenn C∈M, dann M $\vdash$ C
  • (Induktionsschrit)

    wenn M $\vdash$ C₁ und M $\vdash$ C₂, dann M $\vdash$ C₁⊕_yC₂

Beachte Unterschiede:

• Ableitung M $\vdash$ C ist syntaktisch definiert (Term-Umformung)
• Folgerung M $\models$ C ist semantisch definiert (Term-Auswertung)