Korisnik:MisaZvornik/Metod rezolucije

Metod rezolucije

Metod rezolucije je tehnika u logici i računarstvu koja se koristi za dokazivanje tačnosti ili rešavanje problema u formalnim sistemima, posebno u rešavanja logičkih upita.

Osnovni pojmovi

Literali

Literali su najjednostavniji elementi u logici, predtavljaju ili promenjivu (npr. A) ili njenu negaciju (npr. ¬A).

Klauzule

Klauzule su disjunkcije literala, tj. logičko ILI između literala. Koriste se za predstavljanje tvrdnji u logici i obično su sastavljene iz više literala.

Na primer:A∨¬B∨C

Skup klauzula

Kada se formula predsavlja kao skup klauzula, nazivamo to konjuktivnom normalnom formom. Formula je u tom obliku ako predstavlja spoj logičkih I između klauzula.

Na primer: (A∨B)∧(¬A∨C)∧(B∨¬C)

Osnovni princip rezolucije

Rezolucija je proces spajanja klauzula koje sadrže komplementarne literale (tj. literale koji su negacija jedan drugog). Kada nađemo dve klauzule koje sadrže takve literale, možemo ih "rešiti" i dobiti novu klauzulu koja je rezultat njihove kombinacije. Ova nova klauzula ne sadrži komplementarne literale, ali sve ostale informacije iz prvobitnih klauzula su sačuvane.

Na primer, ako imamo klauzule A∨B i ¬A∨C, rezolucijom možemo da uklonimo literale A i ¬A, tako da nam ostaje klauzula B∨C, spajanjem literala B i C.

Značaj rezolucije

1. Automatizovani dokaz teorema - Koristi se kada je potrebno ispitati tačnost neke tvrdnje.

2. Sistemi za rešavanje satisfabilnosti (SAT) - Koristi se za rešavanje problema koji pitaju da li postoji dodela vrednosti promenljivim koje zadovoljavaju neku formulu.

3. Verifikacija softverskih sistema - Koristi se verifikaciji i testiranju računarskih sistema kako bi se proverilo da li se zadovoljavaju određeni bezbednosni i funkcionalni zahtevi.

Efikasnost

Metod rezolucije je jednostavan i efikasan jer računari mogu lako primenjivati rezoluciju na velikim skupovima klauzula, što je korisno u sistemima za dokazivanje teorema ili u rešavanju SAT problema. Takođe, umesto da se pokušava direktno dokazivanje, metod rezolucije koristi indirektni pristup, tj. dokazivanje da ništa ne može biti tačno osim ako sve klauzule ne dovedu do prazne klauzule.

Vidi još