Resolvente

Einfache Sprache

Def. Resolvente

Seien $K$ und $K'$ Klauseln und $X_i$ eine Aussagenlogische Variable mit $X_i\in K$ und $\neg X_i\in K'$. Nennen wir $K$ und $K'$ bezüglich $X_i$ resolvierbar. Die Resolvente $\mathrm{res}_{X_i}(K,K')$ von $K$ und $K'$ bezüglich $X_i$ ist wie folgt definiert

$$\mathrm{res}_{X_i}(K,K') = (K\setminus \{X_i\})\cup (K'\setminus\{\neg X_i\})\;.$$