Neo wird durch den Architekten vor folgende Entscheidung gestellt: Wenn Neo durch die Tür geht, dann kann er seine Lebensabschnittsgefährtin Trinity retten. Wenn Neo nicht durch die Tür geht, dann kann er statt dessen Zion »retten« (in einem sehr rudimentären Sinne, allerdings). Da Neo bei Logik für Informatiker gut aufgepasst hat, verblüfft er den Architekten mit der Erkenntnis, dass er, egal was passiert, Trinity oder Zion retten kann.
Hier ein etwas weniger phantastisches Beispiel ähnlicher Bauart: Ihr persönlicher Vermögensverwalter erklärt Ihnen, dass Sie, wenn Sie jetzt anfangen, für das Alter zu sparen, dann haben Sie im Alter mehr Geld. Auf Nachfrage räumt er dann ein, dass Sie, wenn Sie jetzt nicht anfangen, für das Alter zu sparen, natürlich jetzt mehr Geld haben. Das ist schön, denn immer wenn Sie glauben, Sie hätten zu wenig Geld, so können Sie sich mit einer logischen Folgerung trösten: Egal was passiert, Sie haben jetzt mehr Geld oder im Alter mehr Geld!
Schließlich noch ein Beispiel aus der Technischen Informatik: In einer aufwendigen Untersuchung hat das Forscherteam um Professor Black herausgefunden, dass ein kleiner schwarzer Kasten folgende Eigenschaft hat: Wenn an Pin 1 Strom angelegt ist, dann leuchtet LED 1; wenn hingegen kein Strom angelegt, so leuchtet LED 2. In Rahmen einer Forschungskooperation mit der Theoretischen Informatik hat sich daraufhin herausgestellt, dass man Kraft logischer Schlüsse hieraus folgern kann, dass immer LED 1 oder 2 leuchtet!
Der logischer Gehalt der Folgerungen von Neo, Ihres Vermögensverwalters oder Professor Blacks ist jedes Mal gleich dürftig: Wenn (a -> b) \land (\neg a -> c) gilt, dann gilt b \lor c. Diese eigentlich nicht sonderlich aufregende Erkenntnis hat jedoch einen besonderen Namen: man nennt sie die Resolutionsregel. Sie beschreibt gewissermaßen, was gelten muss »komme was will«. Egal ob Neo durch die Tür geht, egal ob Sie Geld fürs Alter sparen, egal ob Strom anliegt, bestimmte Dinge passieren auf jeden Fall. Es kann dann sein, dass deshalb wieder andere Dinge auf jeden Fall passieren müssen, die wieder andere Dinge nach sich ziehen. Die Resolutionsregel kann man mehrfach anwenden, um herauszufinden, was alles aus einer Menge von Voraussetzungen folgt.
Das wäre alles nicht weiter der Rede wert (es gibt noch viele andere, ähnliche Regeln, die man prinzipiell immer wieder anwenden kann), wenn die Resolutionsregel nicht eine besondere Eigenschaft hätte: Wie wir sehen werden, lässt sich bei jeder kontradiktorischen Formel durch wiederholte Anwendung der Resolutionsregel der innere Widerspruch der Formel irgendwann aufdecken. Daraus kann man im wahrsten Sinne des Wortes »im Handumdrehen« ein Beweissystem basteln, da \neg \phi genau dann kontradiktorisch ist, wenn \phi tautologisch ist.
Wem dieser mathematische Taschenspielertrick zu schnell ging, für den hier das Beweissystem »Resolution« für den Hausgebrauch in einem Satz: »Um zu zeigen, dass \phi tautologisch ist, schreibe \neg \phi in konjunktiver Normalform und wende die Resolutionsregel so lange an, bis ein Widerspruch entsteht.«