Resolutie (logica)

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

In de wiskundige logica en bij automatisch stellingbewijzen is resolutie een afleidingsregel die gebruikt wordt voor bewijzen uit het ongerijmde van zinnen 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.

Resolutieregel[bewerken]

De resolutieregel, waarbij a_i en b_j complementaire literalen zijn:

\frac{
a_1 \lor \ldots \vee a_{i-1} \vee a_i \vee a_{i+1} \vee \ldots \lor a_n, 
\quad b_1 \lor \ldots \vee b_{j-1} \vee b_j \vee b_{j+1} \vee \ldots \lor b_m}
{a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n \lor b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}

Wanneer de twee clausules meer dan één paar complementaire literalen bevatten dan kan de resolutieregel (onafhankelijk) toegepast worden op elk paar om deze te verwijderen. Per keer kan één paar weggehaald worden dus de andere complementaire literalen blijven aanwezig in de overblijvende clausule.

De oorspronkelijke clausules worden niet vervangen door de afgeleide resolvent maar deze clausule wordt gevoegd bij de eerdere clausules. Eén van de redenen hiervoor is dat een clausule meerdere malen nodig kan zijn voor resolutie: het weghalen van een clausule zou er voor kunnen zorgen dat het niet meer mogelijk is de lege clausule af te leiden. Het afleiden van de lege clausule is een manier om te controleren of de clausules onvervulbaar is. Zie resolutie als bewijsstrategie voor een toelichting over het aantonen van onvervulbaarheid met behulp van resolutie.

De bovenstaande regel kan ook met behulp van verzamelingen genoteerd worden:

\frac{ \{ a_1, \ldots, a_{i-1}, a_i, a_{i+1}, \ldots, a_n\}, \{ b_1, \ldots, b_{j-1}, b_j, b_{j+1}, \ldots, b_m\} }{ \{ a_1, \ldots, a_{i-1}, a_{i+1}, \ldots, a_n, b_1, \ldots, b_{j-1}, b_{j+1}, \ldots, b_m \} }

Een verzameling clausules wordt in het Engels een clause set genoemd. Een voordeel van verzamelingen is dat de clausules op deze manier geen identieke literalen bevatten die anders met behulp van regels mogelijk weggewerkt moeten worden.

Voorbeelden van resolutie[bewerken]

Stel we weten dat een auto de kleur rood, blauw of groen heeft. Ook is bekend dat de auto niet blauw is. Als de auto rood, blauw of groen is en niet blauw, dan is deze rood of groen. We kunnen dit in propositielogica weergeven met behulp van de atomaire formules K_{rood}, K_{blauw} en K_{groen}. Met resolutie kunnen we vervolgens afleiden dat de auto rood of groen is:

\frac{K_{rood} \vee K_{blauw} \vee K_{groen}, \quad \neg K_{blauw}}{K_{rood} \vee K_{groen}}

of met behulp van verzamelingen:

\frac{ \{ K_{rood}, K_{blauw}, K_{groen} \}, \{ \neg K_{blauw} \} }{ \{ K_{rood}, K_{groen} \} }

In bovenstaand voorbeeld wordt er een clausule met een enkele literaal gebruikt (¬­K_{blauw}); de enige manier om deze clausule te vervullen is om ¬­K_{blauw} te vervullen, namelijk K_{blauw} = onwaar). De waarheidswaarde van deze atomaire formule is in dit voorbeeld bekend maar het is soms ook mogelijk om waarheidswaarden gaandeweg af te leiden (bijvoorbeeld na enkele resolutiestappen waarbij er clausulen met een enkele literaal overblijven).

Het volgende voorbeeld illustreert dat resolutie ook toegepast kan worden in algemenere situaties (waarin waarheidswaarden niet bekend hoeven te zijn):


\frac{a \vee b, \quad \neg a \vee c}
{b \vee c}

Deze afleiding zegt dat als a of b waar is en dat a onwaar is of c waar is, dan is b of c waar. Als a waar is dan moet c waar zijn om de tweede clausule te vervullen en als a onwaar is dan moet b waar zijn om de eerste clausule te vervullen. Ongeacht de waarheidswaarde van a kan men dus concluderen dat b of c het geval moet zijn.

Resolutie als bewijsstrategie[bewerken]

Resolutie kan gebruikt worden om te bewijzen of een bepaalde conclusie volgt uit één of meerdere premissen. Meer algemeen: met behulp van resolutie kan de onvervulbaarheid van een formule gecontroleerd worden (maar niet de vervulbaarheid). Aangezien elke logische formule omgezet kan worden naar een equivalente[1] formule in de conjunctieve normaalvorm (met behulp van regels zoals de wetten van De Morgan en distributiviteit of andere technieken, zoals het construeren van de Tseitin-transformatie) is het mogelijk een aantal clausules te creëren waarop resolutie (herhaaldelijk) toegepast kan worden. Deze clausules vormen samen een verzameling waarop resolutie toegepast kan worden.

We maken gebruik van een reductio ad absurdum om aan te tonen dat een conclusie wel of juist niet volgt uit de premissen. We nemen aan dat de conclusie niet waar is en we proberen een tegenspraak af te leiden. Wanneer dit lukt dan is de eerder gedane aanname onwaar waardoor we kunnen concluderen dat de conclusie volgt uit de premissen. Deze conclusie is waar indien de premissen ook waar zijn.

Wanneer we, door herhaaldelijk resolutie toe te passen, de lege clausule afleiden, kunnen we concluderen dat de conclusie volgt uit de premissen. Het afleiden van de lege clausule houdt in dat we geen toekenning van waar en onwaar aan de literalen in de clausules hebben kunnen vinden waaronder de formule waar is. Er is dus geen manier om de premissen en de negatie van de conclusie waar te maken waardoor we mogen concluderen dat de conclusie waar is. De lege clausule volgt immers uit twee clausules met daarin de literalen P en ¬P die niet tegelijk waar kunnen zijn waardoor er geen toekenning van waar/onwaar aan de literalen mogelijk is die de gehele verzameling clausules vervult.

Samengevat verloopt een bewijs met behulp van resolutie als volgt:

  1. Allereerst worden de premissen en de conclusie omgezet naar één of meerdere clausules waarop resolutie toegepast kan worden. De premissen en de negatie van de conclusie worden met een logische conjunctie met elkaar verbonden.
  2. Deze conjunctie wordt omgezet naar een equivalente[1] formule in conjunctieve normaalvorm.
  3. Door herhaaldelijk resolutie toe te passen wordt getracht de lege clausule af te leiden. Als dit lukt dan kunnen we concluderen dat de conclusie volgt uit de premissen.

Vereenvoudigen van de verzameling clausules[bewerken]

Tijdens het bewijzen is het mogelijk resolventen af te leiden die niet zinvol zijn voor het produceren van de lege clausule. Zo kan men uit \{\{p\},\{\neg p,q\},\{r\},\{\neg r\}\} bijvoorbeeld de clausule \{q\} afleiden door resolutie toe te passen op de eerste twee clausules maar deze is niet relevant: het toepassen van resolutie op de laatste twee clausules is wel zinvol want dit levert de lege clausule op en daarmee is aangetoond dat de verzameling clausules niet vervulbaar is.

De onderstaande regels maken het mogelijk de verzameling clausules te vereenvoudigen en een verzameling clausules over te houden die vervulbaarheidsequivalent is met de oorspronkelijke verzameling. De afgeleide verzameling hoeft niet logisch equivalent te zijn met de oorspronkelijke verzameling aangezien dit niet noodzakelijk is bij het controleren of de oorspronkelijke verzameling clausules vervulbaar is.

One-literal rule
Wanneer een clausule met één literaal voorkomt, is het mogelijk die clausule en alle clausules waar die literaal in voorkomt te verwijderen. Ook is het mogelijk alle voorkomens van de negatie van die literaal te verwijderen. De clausule met één literaal kan namelijk maar op één manier vervuld worden namelijk door die literaal waar te maken dus alle clausules waar die literaal in voorkomt worden daarmee ook vervuld.
Monotone variable fixing
Wanneer een literaal alleen positief of alleen negatief in de verzameling clausules voorkomt dan is het mogelijk die literaal waar te maken en alle clausules waar die literaal in voorkomt te verwijderen: deze worden namelijk vervuld door die literaal.
Tautologie regel
Clausules waar een literaal en zijn negatie in voorkomen kunnen weggehaald worden aangezien zo'n clausule altijd vervuld kan worden. Voorbeeld: de clausule \{ \ldots, p, \ldots, \neg p, \ldots \} is altijd vervulbaar aangezien zowel bij p = waar als p = onwaar een literaal in de clausule waar is en daardoor is de gehele clausule vervuld.
Subsumptie
Wanneer de literalen van een clausule voorkomen in een grotere clausule dan kan de grotere clausule weggehaald worden aangezien die vervuld wordt als de kleinere clausule ook vervuld wordt. Voorbeeld: er geldt \{ p, q \} \subset \{ p, q, r \} maar aangezien \{ p, q \} vervuld wordt met p = waar of q = waar, is de grotere clausule daarmee ook te vervullen, ongeacht de waarheidswaarde van r.

Een bewijs met behulp van binaire resolutie[bewerken]

Stel we willen het volgende aantonen:

P: Het regent (premisse 1).
P \to Q: Als het regent dan worden de straten nat (premisse 2).
Q: De straten worden nat (conclusie).

Op basis van de twee premissen (P, P \to Q) concluderen we dat de straten nat worden (Q). Deze redenering is geldig en staat bekend als modus ponens. Dit kan met behulp van binaire resolutie als volgt worden aangetoond:

  1. De premissen en de negatie van de conclusie worden met een conjunctie met elkaar verbonden:
    P \wedge (P \rightarrow Q) \wedge \neg Q
  2. Omzetting naar conjunctieve normaalvorm:
    P \wedge (\neg P \vee Q) \wedge \neg Q
    \{\{P\},\{\neg P, Q\}, \{\neg Q\} \} (genoteerd met behulp van verzamelingen)
  3. Door binaire resolutie toe te passen, kunnen we de lege clausule afleiden (eerst op P en ¬P en vervolgens Q en ¬Q of andersom):
    1. \{\{P\},\{\neg P, Q\}, \{\neg Q\} \}
    2. \{\{P\},\{\neg P, Q\}, \{\neg Q\}, \{Q\} \} (binaire resolutie op eerste en tweede clause)
    3. \{\{P\},\{\neg P, Q\}, \{\neg Q\}, \{Q\}, \{\} \} (binaire resolutie op derde en vierde clause)

Geschiedenis[bewerken]

Resolutie werd in 1965 door John Alan Robinson gepresenteerd in A machine-oriented logic based on the resolution principle in Journal of the ACM. Deze publicatie betekende een doorbraak in het automatisch stellingbewijzen en veel hedendaagse automatische stellingbewijzers zijn gebaseerd op dit principe. Resolutie is momenteel de krachtigste methode om de onvervulbaarheid van een formule aan te tonen.

Voorlopers van resolutie zijn de Davis-Putnam procedure (DPP, 1960) en het Davis-Putnam-Logemann-Loveland algoritme (DPLL, 1962), een verbetering van DPP. Beide algoritmen maken gebruik van hetzelfde principe: men kiest een literaal (bijvoorbeeld p) en splitst de verzameling in twee verzamelingen: één waarin p geldt en één waarin ¬p geldt. In de Davis-Putnam procedure worden de beide verzamelingen weer samengevoegd met distributiviteitswetten maar bij DPLL gebeurt dit niet: het algoritme wordt op beide verzamelingen recursief toegepast waardoor een boomstructuur ontstaat. Als de oorspronkelijk verzameling clausules onvervulbaar was dan zal het algoritme bij ten minste één van de bladeren de lege clausule afleiden (en daarmee aantonen dat de verzameling clausules onvervulbaar is). Wanneer een afgesplitste verzameling clausules vervulbaar is (waarin bijvoorbeeld p waar is) dan is de oorspronkelijke verzameling clausules dat ook (met p waar).

Soorten resolutie[bewerken]

Er bestaan verschillende soorten resolutie:[2]

Binaire resolutie
De resolvent is afkomstig uit precies twee clausules.
Unit resolution
Bij unit resolution moet ten minste één clausule die bij resolutie gebruikt wordt, bestaan uit precies één literaal. Unit resolution dient niet verward te worden met de one-literal rule en ook niet met unit-resulting resolution (UR-resolution, zie hieronder).
Lineaire resolutie
Iedere geproduceerde resolvent wordt meteen weer gebruikt voor resolutie.
Semantische resolutie
Met behulp van een model wordt de verzameling clausules verdeeld in twee verzamelingen, namelijk in een verzameling die door het model vervuld wordt en de rest (de clausules die niet door het model vervuld worden). Resolventen mogen alleen geproduceerd worden als uit beide verzamelingen een clausule wordt gebruikt.
Geordende semantische resolutie
Hetzelfde als semantische resolutie maar de nu met een ordening op de literalen in de clausules (bijvoorbeeld op alfabetische volgorde). Wanneer resolutie toegepast wordt mag alleen de kleinste/eerste literaal gebruikt worden uit een clausule uit de verzameling clausules die door het model gefalsifieerd wordt.
Positieve hyperresolutie
Eén of meerdere clausules met alleen positieve literalen, satellieten genoemd, worden gebruikt bij resolutie op een clausule met éen of meerdere negatieve literalen, de nucleus. Deze nucleus kan ook positieve literalen bevatten. Het toepassen van resolutie wordt hierbij ook wel clashen genoemd. Bij positieve hyperresolutie bestaan zowel de satellieten als de resolvent geheel uit positieve literalen. Hyperresolutie is eigenlijk meerdere binaire resolutiestappen tegelijk maar er worden geen tussenliggende clausulen geproduceerd. Zonder verdere aanduiding wordt met hyperresolutie positieve hyperresolutie bedoeld.
Negatieve hyperresolutie
Bij negatieve hyperresolutie bestaan de satellieten uit alleen negatieve literals en bevat de nucleus één of meerdere positieve literalen. De resolvent bestaat alleen uit negatieve literalen.
Unit-resulting resolutie (UR-resolutie)
Bij UR-resolution worden satellieten gebruikt die bestaan uit 1 literaal en de verkregen resolvent dient ook uit 1 literaal te bestaan. UR-resolution lijkt op hyperresolutie alleen wordt er nu gekeken naar het aantal literalen in de satellieten en de resolvent en niet naar het feit of er alleen positieve of negatieve literalen aanwezig zijn in de gebruikte clausulen. In de varianten positieve UR-resolutie en negatieve UR-resolutie dient de resolvent een unit clausule te zijn met een positieve respectievelijk negatieve literaal.

Voorbeelden[bewerken]

In de onderstaande voorbeelden wordt de notatie C_0 \ldots C_n \Rightarrow R gebruikt om aan te duiden dat de resolvent R wordt verkregen uit de clausulen C_0 \ldots C_n.

Binaire resolutie
\{ p, \neg q \}, \{ \neg p, r \} \Rightarrow \{ \neg q, r \}
Unit resolution
\{ p \}, \{ \neg p, s, t \} \Rightarrow \{ s, t\}
Positieve hyperresolutie
\{ p \}, \{ q, r, s \} \text{ (satellieten) } \{ \neg p, \neg q, t \} \text{ (nucleus) } \Rightarrow \{ r, s, t \}
Negatieve hyperresolutie
\{ \neg p \}, \{ \neg q, \neg r, \neg s \} \text{ (satellieten) } \{ p, q, \neg t \} \text{ (nucleus) } \Rightarrow \{ \neg r, \neg s, \neg t \}
Positieve UR-resolutie
\{ p \}, \{ \neg q \} \text{ (satellieten) } \{ \neg p, q, r \} \text{ (nucleus) } \Rightarrow \{ r \}
Negatieve UR-resolutie
\{ p \}, \{ \neg q \} \text{ (satellieten) } \{ \neg p, q, \neg r \} \text{ (nucleus) } \Rightarrow \{ \neg r \}

Resolutie in eerste-ordelogica[bewerken]

Resolutie in eerste-ordelogica maakt gebruik van unificatie, het aan elkaar gelijk maken van predicaten. Dit kan door variabelen of predicaten in te vullen in variabelen in predicaten, dit wordt substitutie genoemd. Zo kunnen de predicaten P(x) en ¬P(y) met elkaar geünificeerd worden door de variabele x in te vullen op de plaats waar y staat. Dit kan genoteerd worden als x/y. Na deze substitutie verkrijgen we de predicaten P(x) en ¬P(x) waar resolutie op toegepast kan worden.

Voetnoten[bewerken]

  1. a b De formule in conjunctieve normaalvorm hoeft niet logisch equivalent te zijn, een vervulbaarheidsequivalente formule is voldoende aangezien we de vervulbaarheid van de formule willen achterhalen.
  2. Strikt gezien zijn het beperkingen op de mogelijke resolutiestappen die toegepast kunnen worden.

Referenties[bewerken]

  • J. A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the ACM, Volume 12, Number 1, p. 23-41, januari 1965

Externe link[bewerken]