Resolution (Logik)
Die Resolution der Aussagenlogik ist ein Verfahren, um eine Formel F, die in konjunktiver Normalform vorliegt, auf Erfüllbarkeit und Gültigkeit zu testen.Dabei sind folgende Aussagen möglich:
- führt Res(F) zu einem Widerspruch, ist F unerfüllbar
- führt Res(-F) zu einen Widerspruch, ist F gültig