One-literal rule
Bij automatisch stellingbewijzen is de one-literal rule (OLR) of unit propagation (UP) een methode om een verzameling clausules (Engels: een clause set) te vereenvoudigen en 'op te schonen'. De one-literal rule houdt in dat wanneer een verzameling clausules een clausule bevat met één literal dan is het mogelijk die clausule en alle clausules waar die literal in voorkomt te verwijderen en alle voorkomens van de negatie van de literal te verwijderen.
Definitie bewerken
Formeel houdt de one-literal rule in dat uit
- ,
- waarbij p en ¬p niet voorkomen in ,
de volgende verzameling clausules mag worden afgeleid:
- .
De enige manier om een clausule met één literal te vervullen is om die literal waar te maken. De clausules waar die literal in voorkomt, zijn hierdoor ook waar aangezien een clausule, een disjunctie, waar is als een van de disjuncten waar is. De voorkomens van ¬p kunnen weggehaald worden aangezien deze onwaar zijn (want p moet waar zijn) maar de overige literals van een clausule waar ¬p in voorkomt, kunnen niet weggehaald worden aangezien één of meer van die literals waar moet zijn om die clausule te vervullen.
Kenmerken bewerken
Een belangrijke eigenschap die deze regel mogelijk maakt is dat de afgeleide verzameling clausules vervulbaar is als de oorspronkelijke verzameling dat ook was en niet vervulbaar als de oorspronkelijke verzameling dat ook niet was. Anders geformuleerd, de beiden verzamelingen clausules zijn vervulbaarheidsequivalent.
Een automatische stellingbewijzer die gebruikmaakt van resolutie kan clausules toevoegen aan de verzameling die niet noodzakelijkerwijs bijdragen aan het afleiden van de lege clausule en daarmee het bewijzen van de stelling (zie Resolutie als bewijsstrategie voor een toelichting hierover). Een vereenvoudigde verzameling clausules heeft als voordeel dat het aantal mogelijkheden om resolutie toe te passen beperkt wordt en daarmee ook de mogelijkheden om niet bruikbare clausules af te leiden.
Verschil met unit resolution bewerken
De one-literal rule dient niet verward te worden met unit resolution. Bij unit resolution wordt resolutie toegepast op een clausule met exact 1 literal: hierna wordt een clausule toegevoegd aan de verzameling clausules. Bij unit resolution worden dus geen clausules weggehaald terwijl dit bij de one-literal rule wel gebeurt.
Ook is het zo dat de verzameling clausules na unit resolution equivalent is aan de verzameling waar men mee begon (er is een clausule toegevoegd maar deze is gevormd uit bestaande clausules) terwijl bij de one-literal rule de resulterende verzameling clausules alleen vervulbaarheidsequivalent is met de voorgaande verzameling.