Unit propagation (UP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of clauses.

PropertyValue
dbpprop:abstract
  • Unit propagation (UP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of clauses.
  • Bij automatisch stelling bewijzen is de one-literal rule (OLR) of unit propagation (UP) een methode om een verzameling clausules 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. 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 gebruik maakt 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. 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 één 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.
dbpprop:hasPhotoCollection
rdfs:comment
  • Unit propagation (UP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of clauses.
  • Bij automatisch stelling bewijzen is de one-literal rule (OLR) of unit propagation (UP) een methode om een verzameling clausules 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.
rdfs:label
  • Unit propagation
  • One-literal rule
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of