resolutie

In de wiskundige logica en bij is resolutie een afleidingsregel die gebruikt wordt voor bewijzen uit het ongerijmde van in de propositie- en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule (Engels: clause, een disjunctie van literalen) uit twee clausules die complementaire literalen bevatten. De resolutieregel produceert een nieuwe clausule met alle literalen in beide clausules behalve de complementaire literalen. De geproduceerde clausule wordt een resolvent genoemd. Resolutie wordt in automatische stellingbewijzers gebruikt om de onvervulbaarheid, het ontbreken van een toekenning van waar of onwaar aan de atomaire formules zodat de formule waar is, van een logische formule te bewijzen. Meer informeel gezegd probeert men aan te tonen dat de formule niet waar kan zijn.