Brontekst bekijken van One-literal rule

Bij [[automatisch stellingbewijzen]] is de '''one-literal rule''' ('''OLR''') of '''unit propagation''' ('''UP''') een methode om een [[Verzameling (wiskunde)|verzameling]] [[Clausule (logica)|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 [[Logische negatie|negatie]] van de literal te verwijderen.

== Definitie ==

Formeel houdt de one-literal rule in dat uit

:<math>\{\{p\}, \{p\} \cup A_{1}, \dots, \{p\} \cup A_{k}, \{\neg p\} \cup B_{1}, \dots \{\neg p\} \cup B_{l}, C_{1}, \dots, C_{m} \}</math>,

::waarbij ''p'' en ''¬p'' niet voorkomen in <math>C_{1}, \dots, C_{m}</math>,

de volgende verzameling clausules mag worden afgeleid:

:<math>\{ B_{1}, \dots, B_{l}, C_{1}, \dots, C_{m} \}</math>.

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 [[Logische disjunctie|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 ==

Een belangrijke eigenschap die deze regel mogelijk maakt is dat de afgeleide verzameling clausules [[Vervulbaarheid|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 [[vervulbaarheidsequivalentie|vervulbaarheidsequivalent]].

Een automatische stellingbewijzer die gebruikmaakt van [[resolutie (logica)|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 (logica)#Resolutie als bewijsstrategie|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 ===

De one-literal rule dient niet verward te worden met [[Resolutie (logica)|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.

== Zie ook ==
*[[Monotone variable fixing]]
*[[Resolutie (logica)|Resolutie]]
*[[DPLL-algoritme]]

[[Categorie:Automatisch redeneren]]
[[Categorie:Afleidingsregel]]