Бұдан G формуласы F1, және F2 логикалық формуласын шығады.
Бірінші қатарлы логикаға көшейік. Айнымалыға байланысты дизъюнктке тапсырыс берейік, ол жалпы кванторлармен байланыста болады, бірақ кванторларды өіміз жазбаймыз. Бұдан шығады, екі бірдей айнымалы әртүрлі дизъюнкттарда әртүрлі болады.
Байқайтын болсақ, бірінші қатарлы логикада резолюция ережесінің бұл түрі орындалмайды. Расында да S={P(x),ØP(a)} дизъюнкттар жиыны орындалмайды, (себебі х айнымалысы жалпы квантормен байланысты). Осы уақытта егер логикалық құралдар үшін резолюция ережесін қолдансақ, онда S бос дизъюнктін ала алмаймыз. Бұл жағдайда не істеу керек. P(x) дизъюнктін кез келген х үшін P(x) ақиқат, бірақ P(x) ақиқат болады және x=a үшін де. х=а деп алсақ , S/={P(a),ØP(a)} дизъюнкттар жиынын аламыз. S жиыны және S/ бір мезетте орындалады (немесе орындалмайды). S/ ішінен бастапқы резолюция ережесінің көмегімен тривиалды түрі шығады. Бұл мысалда бірінші қатарлы логикадағы резолюция ережесіне қосымша мүмкіндіктер қосу қажет екендігін көрсетеді.
Қажетті тұжырымдар берейік.
Анықтама. Ауыстыру деп теңсіздіктер жиыны аталады s={x1=t1, x2=t2,…, xn=tn},
x1,x2,…,xn – әртүрлі айнымалы, t1,t2,…,tn – терм, ti термінде xi (1£ i £ n) айнымалысы жоқ.
Егер s = (x1=t1,...,xn=tn), ал F – дизъюнкт, s(F) арқылы дизъюнкті белгілейміз, F бірқалыпты айнымалыдан шыққан x1 –ден t1; және т.б. xn -нен tn. Мысал, егер s={x1=f(x2), x2=c, x3=g(x4)), F=R(x1,x2,x3)ÚØP(f(x2)), онда s(F)=R(f(x2), c, g(x4))ÚØP(f(c). Термдер осы сияқты орындалады.
Ыңғайлы болуы үшін бос ауыстыру енгізейік, теңсіздігі жоқ. Бос ауыстыруды е арқылы белгілейік.
Достарыңызбен бөлісу: |
