Resolutie (logica)

Van Wikipedia

In wiskundige logica en bij automatisch stelling bewijzen is resolutie is een afleidingsregel die gebruikt wordt bij reductio ad absurdum bewijzen voor zinnen in propositielogica en predicatenlogica. Resolutie is een geldige regel voor het afleiden van een nieuwe clausule (Engels: clause, een disjunctie van literals) uit twee clausules die complementaire literals bevatten. De resolutieregel produceert een nieuwe clausule met alle literals in beide clausules behalve de complementaire literals. 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. Om te bewijzen dat een formule vervuld kan worden zijn andere technieken nodig, zoals semantische tableaus of zogeheten satisfiability checkers die een toekenning van waar of onwaar proberen te vinden zodat de formule waar wordt.

Inhoud

1 Resolutieregel
- 1.1 Voorbeeld van resolutie
2 Resolutie als bewijsstrategie
- 2.1 Vereenvoudigen van de verzameling clausules
- 2.2 Een bewijs met behulp van binaire resolutie
3 Geschiedenis
4 Soorten resolutie
5 Resolutie in eerste-ordelogica
6 Voetnoten
7 Referenties
8 Externe links

[bewerk] Resolutieregel

De resolutieregel, waarbij $a i$ en $b j$ complementaire literals 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 literals 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 literals 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 literals bevatten die anders met behulp van regels mogelijk weggewerkt moeten worden.

[bewerk] Voorbeeld van resolutie

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 r o o d$ , $K b l a u w$ en $K g r o e n$ . 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} \} }$

[bewerk] Resolutie als bewijsstrategie

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 afgeleide) 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 en waar is indien de premissen ook waar zijn.

Waneer 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 literals 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 literals P en ¬P die niet tegelijk waar kunnen zijn waardoor er geen toekenning van waar/onwaar aan de literals mogelijk is die de gehele verzameling clausules vervult.

Samengevat verloopt een bewijs met behulp van resolutie als volgt:

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.
Deze conjunctie wordt omgezet naar een equivalente^[1] formule in conjunctieve normaalvorm.
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.

[bewerk] Vereenvoudigen van de verzameling clausules

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},{¬p, q},{r},{¬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 literal voorkomt, is het mogelijk die clausule en alle clausules waar die literal in voorkomt te verwijderen. Ook is het mogelijk alle voorkomens van de negatie van die literal te verwijderen. De clausule met één literal kan namelijk maar op één manier vervuld worden namelijk door die literal waar te maken dus alle clausules waar die literal in voorkomt worden daarmee ook vervuld.
Monotone variable fixing: Wanneer een literal alleen positief of alleen negatief in de verzameling clausules voorkomt dan is het mogelijk die literal waar te maken en alle clausules waar die literal in voorkomt te verwijderen: deze worden namelijk vervult door die literal.
Tautologie regel: Clausules waar een literal en zijn negatie in voorkomen kunnen weggehaald worden aangezien zo'n clausule altijd vervuld kan worden.
Subsumptie: Wanneer de literals 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.

[bewerk] Een bewijs met behulp van binaire resolutie

Stel we willen het volgende aantonen:

P: Het regent (premisse 1).

P → 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 → 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:

De premissen en de negatie van de conclusie worden met een conjunctie met elkaar verbonden:

$P \wedge (P \rightarrow Q) \wedge \neg Q$
Omzetting naar conjunctieve normaalvorm:

$P \wedge (\neg P \vee Q) \wedge \neg Q$

$\{\{P\},\{\neg P, Q\}, \{\neg Q\} \}$ (genoteerd met behulp van verzamelingen)
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)

[bewerk] Geschiedenis

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 stelling bewijzen 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 literal (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 tenminste éé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).

[bewerk] Soorten resolutie

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 literal.
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 literals in de clausules (bijvoorbeeld op alfabetische volgorde). Wanneer resolutie toegepast wordt mag alleen de kleinste/eerste literal 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 literals, satellieten genoemd, worden gebruikt bij resolutie op een clausule met éen of meerdere negatieve literals, de nucleus. Het toepassen van resolutie wordt hierbij ookwel clashen genoemd.
Negatieve hyperresolutie: Bij negatieve hyperresolutie bestaan de satellieten uit alleen negatieve literals en bevat de nucleus één of meerdere positieve literals.

[bewerk] Resolutie in eerste-ordelogica

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.

[bewerk] Voetnoten

↑ ^1,0 ^1,1 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.
↑ Strict gezien zijn het beperkingen op de mogelijke resolutiestappen die toegepast kunnen worden.

[bewerk] Referenties

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

[bewerk] Externe links

(en) Resolution Principle op MathWorld.

Categorieën: Logica | Automatisch redeneren