Monotone variable fixing
Bij automatisch stelling bewijzen is monotone variable fixing (ook bekend als de pure literal rule) een methode om een verzameling clausules (Engels: een clause set) te vereenvoudigen en 'op te schonen'. Monotone variable fixing houdt in dat wanneer een literal alleen positief of alleen negatief voorkomt het mogelijk is die literal waar te maken en alle clausules waar die literal in voorkomt uit de verzameling clausules te verwijderen.
Definitie bewerken
Formeel houdt monotone variable fixing in dat uit
- ,
- waarbij ¬p niet voorkomt in ,
de volgende verzameling clausules mag worden afgeleid:
- .
Een analoge definitie geldt voor het geval dat alleen ¬p voorkomt en dat p niet voorkomt in .
Een clausule die een literal bevat die niet complementair is met een literal uit een andere clausule kan niet met behulp van resolutie weggehaald worden. De enige manier om die clausule te vervullen is om die literal waar te maken en de clausule te verwijderen. Hier komt ook de naam monotone variable fixing vandaan: de waarheidswaarde van een variabele wordt vastgelegd (gefixeerd). De term monotone geeft aan dat de waarheidswaarde vastgelegd wordt en dat deze niet later in het proces nog veranderd kan worden.
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.