Корисник:MisaZvornik/Метод резолуције

Метод резолуције

Метод резолуције је техника у логици и рачунарству која се користи за доказивање тачности или решавање проблема у формалним системима, посебно у решавања логичких упита.

Основни појмови

Литерали

Литерали су најједноставнији елементи у логици, предтављају или промењиву (нпр. А) или њену негацију (нпр. ¬А).

Клаузуле

Клаузуле су дисјункције литерала, тј. логичко ИЛИ између литерала. Користе се за представљање тврдњи у логици и обично су састављене из више литерала.

На пример:A∨¬B∨C

Скуп клаузула

Када се формула предсавља као скуп клаузула, називамо то коњуктивном нормалном формом. Формула је у том облику ако представља спој логичких И између клаузула.

На пример: (A∨B)∧(¬A∨C)∧(B∨¬C)

Основни принцип резолуције

Резолуција је процес спајања клаузула које садрже комплементарне литерале (тј. литерале који су негација један другог). Када нађемо две клаузуле које садрже такве литерале, можемо их "решити" и добити нову клаузулу која је резултат њихове комбинације. Ова нова клаузула не садржи комплементарне литерале, али све остале информације из првобитних клаузула су сачуване.

На пример, ако имамо клаузуле A∨B и ¬A∨C, резолуцијом можемо да уклонимо литерале A и ¬A, тако да нам остаје клаузула B∨C, спајањем литерала B и C.

Значај резолуције

1. Аутоматизовани доказ теорема - Користи се када је потребно испитати тачност неке тврдње.

2. Системи за решавање сатисфабилности (САТ) - Користи се за решавање проблема који питају да ли постоји додела вредности променљивим које задовољавају неку формулу.

3. Верификација софтверских система - Користи се верификацији и тестирању рачунарских система како би се проверило да ли се задовољавају одређени безбедносни и функционални захтеви.

Ефикасност

Метод резолуције је једноставан и ефикасан јер рачунари могу лако примењивати резолуцију на великим скуповима клаузула, што је корисно у системима за доказивање теорема или у решавању САТ проблема. Такође, уместо да се покушава директно доказивање, метод резолуције користи индиректни приступ, тј. доказивање да ништа не може бити тачно осим ако све клаузуле не доведу до празне клаузуле.

Види још