Кіріспе

Джон Маккарти жасаған монотонды емес логика. Айналым – Джон Маккарти жасаған монотонды емес логика, егер басқаша көрсетілмесе, нәрселер күтілгендей болады деген жалпы түсініктерді формалдау үшін құрылған. Кейіннен Маккарти айналымды кадрлық проблеманы шешу үшін пайдаланды. Айналымды бастапқы тұжырымдамасы бойынша іске асыру үшін Маккарти бірінші реттік логиканы кейбір предикаттардың кеңеюін азайтуға мүмкіндік беретіндей етіп кеңейтті, мұнда предикаттың кеңеюі – бұл предикаттың шындыққа сай келетін мәндердің жиынтығы. Бұл азайту, жабық әлем туралы болжамға ұқсас, яғни шындық деп белгілі емес нәрсе жалған деп есептеледі. Маккарти қарастырған бастапқы мәселе – миссионерлер мен каннибальдардың мәселесі: өзеннің бір жағалауында үш миссионер және үш каннибал бар; олар тек екеуін сыйдыратын қайықпен өзенді кесіп өтуі керек, сонымен қатар каннибальдар ешқашан екі жағалаудың екеуінде де миссионерлерден көп болмауы керек (әйтпесе миссионерлер өлтіріліп, ықтимал, желінеді). Маккарти қарастырған мәселе – мақсатқа жету үшін қадамдар тізбегін табу емес (миссионерлер мен каннибальдардың мәселесі туралы мақалада осындай шешім бар), керісінше, нақты айтылмаған жағдайларды жою. Мысалы, «оңтүстікке жарты миль жүріп, көпір арқылы өзенді кесіп өту» шешімі интуитивті түрде жарамсыз, өйткені мәселенің шартында мұндай көпір туралы ештеңе айтылмаған. Екінші жағынан, мәселенің шартында бұл көпірдің болуы да жоққа шығарылмаған. Көпірдің жоқ болуы – мәселенің шартында оның шешіміне қатысты барлық маңызды ақпарат бар деген тұжырымның салдары. Көпір жоқ екенін нақты айту бұл мәселені шешпейді, себебі жою керек басқа да көптеген ерекше жағдайлар бар (мысалы, каннибальдарды байлап қоюға арқанның болуы, жақын жерде үлкен қайықтың болуы және т.б.). Кейіннен Маккарти инерцияның түсінігін формалдау үшін айналымды пайдаланды: басқаша көрсетілмесе, заттар өзгермейді. Айналым, жағдайларды өзгертетінін нақты білетін әрекеттерден басқа барлық әрекеттер жағдайларды өзгертетінін нақты көрсетуден аулақ болу үшін пайдалы болып көрінді; бұл кадрлық проблема деп аталады. Алайда, Маккарти ұсынған шешім кейбір жағдайларда, мысалы, Йельдегі атыс оқиғасында, дұрыс емес нәтижелерге әкелетіні кейіннен көрсетілді. Фреймдік проблеманы шешудің басқа да жолдары бар, олар Йельдегі атыс проблемасын дұрыс формалдайды; кейбіреулері айналымды, бірақ басқаша қолданады.

Предикатты округ

Маккарти ұсынған шектелудің бастапқы анықтамасы бірінші реттік логикаға қатысты. Пропозициялық логикада (ақиқат немесе жалған бола алатын нәрсе) айнымалылардың атқаратын рөлін бірінші реттік логикада предикаттар орындайды. Яғни, ұйғарымдық формула бірінші реттік логикада әр ұйғарымдық айнымалыны нөлдік аритметикалық предикатпен (яғни, аргументі жоқ предикатпен) алмастыру арқылы беріле алады. Сондықтан, минимизациялау бірінші реттік логика нұсқасындағы шектелуде предикаттарға қатысты жүзеге асырылады: формуланың шектелуі мүмкін болған жағдайда предикаттарды жалған мәніне ие болуға мәжбүрлеу арқылы алынады. Предикатты қамтитын бірінші реттік логикалық формула берілген болса, осы предикатты шектеу – мәндердің ең кішкентай жиынында ғана предикатқа шындық мәні тағайындалатын модельдерді таңдаумен тең. Формальды түрде, бірінші реттік модельдегі предикаттың кеңеюі – бұл модельдегі предикаттың шындыққа тағайындаған мәндер жиыны. Бірінші реттік модельдерде әрбір предикат символының бағалануы болады; мұндай бағалау предикаттың оның аргументтерінің кез келген мүмкін мәні үшін шын немесе жалған екенін көрсетеді. Предикаттың әрбір аргументі термин болуы керек, ал әрбір термин бір мәнге бағаланады, сондықтан модельдер кез келген мәндер жиыны үшін шындық мәнін көрсетеді. Модельдегі кеңею – бұл модельде шындыққа сәйкес келетін терминдер жиыны. Формуладағы предикатты шектеу тек қана осы предикаттың кеңеюі ең кішкентай болатын модельдерді таңдау арқылы жүзеге асырылады. Мысалы, егер формула тек екі модельге ие болса, олардың арасындағы айырмашылық тек қана предикаттың біреуінде шындық, екіншісінде жалған болуында болса, онда тек екінші модель таңдалады. Себебі бірінші модельде предикат кеңеюіне кіреді, ал екіншісінде кірмейді. Маккартидің бастапқы анықтамасы семантикалық емес, синтаксикалық сипатта болды. Формула және предикат берілген жағдайда, предикатты шектеу келесі екінші реттік формула арқылы жүзеге асырылады:

Бұл формуланың предикаты сол предикаттың аритметикалық сипаттамасына ие. Бұл екінші реттік формула, өйткені ол предикатқа қатысты квантификацияны қамтиды. Субформула келесінің қысқартылған түрі болып табылады:

Бұл формула n – терминдердің жиынтығын білдіреді, мұнда n – предикаттың аритметикасы. Бұл формула кеңеюді минимизациялау қажеттігін көрсетеді: модельдің шындық бағалауын қарастыру үшін, басқа ешқандай предикат осы предикаттың жалған мәніне ие болатын әрбір жиынтыққа жалған мәнін тағайындамайынша, одан өзгеше болуы керек. Бұл анықтама тек бір предикатты шектеуге мүмкіндік береді. Бірнеше предикатқа қатысты кеңею тривиальды болса да, бір предикаттың кеңеюін минимизациялаудың маңызды қолданылуы бар: нәрселердің әдетте күтілгендей болатыны туралы идеяны түсіру. Бұл идеяны жағдайлардың қалыптан тыс екенін білдіретін бір предикатты минимизациялау арқылы формальды түрде беруге болады. Әсіресе, әрбір белгілі факт логикалық түрде, тек қалыпты жағдайларда ғана орынды екенін көрсететін сөзбе-сөз мәлімдемемен көрсетіледі. Осы предикаттың кеңеюін минимизациялау нәрселердің күтілгендей (яғни, қалыптан тыс емес) екені туралы тұжырымға негізделуге мүмкіндік береді және бұл тұжырым тек мүмкін болған жағдайда ғана жасалады (қалыптан тыс жағдайлар фактілерге қайшы келмесе ғана жалған деп есептелуі мүмкін).

Нысанды шектеу

Нүктелік шеңбер – Владимир Лифшиц енгізген бірінші реттік шеңбердің бір түрі. Нүктелік шеңбердің мағынасы – предикаттың кеңейтуін ең төмендетудің орнына, әрбір мәндер жұбы үшін предикаттың мәнін жеке-жеке ең төмендетуде. Мысалы, домені бар екі модель бар, біреуінде , екіншісінде . Бірінші модельдегі кеңейту , ал екіншісіндегі кеңейту болғандықтан, шеңберлеу тек бірінші модельді таңдайды. Пропозициялық жағдайда нүктелік және предикаттық шеңберлеу бірдей. Нүктелік шеңберлеуде әрбір мәндер жұбы жеке қарастырылады. Мысалы, формуласында , егер формула орындалатын жағдайда кез келген мәнді шыннан жалғанға өзгерту мүмкін болмаса, ғана минималды модель деп есептеледі. Нәтижесінде, нүктелік шеңберлеуде модельі таңдалады, себебі тек -ты жалғанға өзгерту формуланың орындалуын бұзады, және сол сияқты -ға да қатысты.

Домен мен формуланың шектелуі

Маккартидің бұрынғы шектеу ұғымы предикаттардың кеңеюінен гөрі бірінші реттік модельдердің доменін азайтуға негізделген. Яғни, егер модельдің домені кішірек болса және екі модель ортақ мәндер жиынын бағалауда сәйкес келсе, онда ол модель екіншісінен кем деп есептеледі. Формулалық шектеу – Маккарти ұсынған кейінірек пайда болған формализм. Бұл предикат кеңеюі емес, формуланың кеңеюін азайту арқылы шектеуді жалпылау болып табылады. Басқаша айтқанда, формула сондай етіп берілуі мүмкін, оның домендегі мәндер жиыны, формулаға сәйкес келетін, ең кішкентай болады.