Satz Vollständigkeit der aussagenlogischen Resolution

Einfache Sprache

Def. Satz Vollständigkeit der aussagenlogischen Resolution

Sei $M$ eine Menge von Klauseln. Es gilt $\{\bigvee K\mid K\in M\}$ ist unerfüllbar genau dann, wenn $\emptyset$ sich aus $M$ per Resolution herleiten lässt.