|
|
Pravilo rezolucije za iskazni račun
Rezolucijska metoda opovrgavanja zasniva se na sledećem pravilu rezolucije:
(R)
A,B,C su bilo koje iskazne formule
, 
, tj iz 'not'A i A izvodi se kontradikcija
Korektnost pravila R znači da se primenom pravila R na formule F1 i F2 dobija formula F koja je logička posledica formula F1 i F2 tj. F1,F2 |--- F . Ako su F1 i F2 teoreme računa L ,onda je formula F, izvedena rezolucijom, teorema u L. Potpunost pravila R znači da se svaka teorema računa L može dokazati primenom pravila R, umesto pravila MP.
Stav korektnosti pravila rezolucije : Pravilo R je korektno pravilo izodjenja u iskaznom računu.Dokaz: U iskaznom racunu L sa pravilom MP za bilo koje formule A,B,C važi: 'not'A V B, A V C |--- 'not'B=>C .Koristeći definiciju simbola V u teoriji L možemo pisati: A=>B, 'not'A=>C |--- 'not'B=>C , što se pomoću MP u računu L može izvesti na sledeće načine:
• A=>B hipoteza
• 'not'A=>C hipoteza
• (A=>B)=>('not'B=> 'not'A) aksioma A2 i teorema A<=> 'not''not'A
• 'not'B=>'not'A 1,3 po MP
• 'not'B=>C iz stava 2 iskaznog računa
Stav potpunosti pravila rezolucije :Pravilo R je potpuno pravilo izvodjenja u iskaznom računu.
Dokaz: Primenom pravila R može se izvesti svaka teorema računa L. Neka iz formula F1,F2 primenom MP izvedena formula F. Tada jedna od formula ima oblik A,druga A=>B , pri čemu je F formula B. Zamenimo li po definiciji implikaciju A=>B formulom 'not'AVB, tada se iz A, 'not'AVB primenom pravila R izvodi formula B. Na taj način, svako izvodjenje primenom MP postaje izvodjenje primenom R.