Resolvente

#Studium #Informatik #Logik #Definition

Gegeben zwei Klauseln $C_{1}$ und $C_{2}$ und ein Literal $L$ , für das gilt $L \in C_{1}$ und $\bar{L} \in C_{2}$ , ist die Resolvente die neue Klausel, die durch die Vereinigung der beiden Klauseln ohne das komplementäre Literalpaar entsteht:

C_{r e s} = (C_{1} ∖ {L}) \cup (C_{2} ∖ {\bar{L}})