Сәтсіздік ретінде теріске шығару - Negation as failure

Сәтсіздік ретінде теріске шығару (NAF, қысқаша) - бұл монотонды емес қорытынды ереже логикалық бағдарламалау, шығару үшін қолданылады (яғни бұл ұстамайды деп болжанған) туындай алмауынан . Ескертіп қой мәлімдемеден өзгеше болуы мүмкін туралы логикалық теріске шығару туралы байланысты толықтығы қорытынды алгоритмінің, сонымен қатар формальды логикалық жүйенің.

Сәтсіздік деп теріске шығару екеуінің де алғашқы күндерінен бастап логикалық бағдарламалаудың маңызды ерекшелігі болды Жоспарлаушы және Пролог. Prolog-да ол әдетте Prolog-тің экстралогиялық құрылымдарын қолдану арқылы жүзеге асырылады.

Жоспарлаушы семантикасы

Жоспарлаушыда сәтсіздікке байланысты теріске шығару келесідей жүзеге асырылуы мүмкін:

егер (емес (мақсат р)), содан кейін (бекіту ¬p)

егер бұл толық іздеу болса, дәлелдеуге болады дейді б сәтсіздікке ұшырады, содан кейін бекітіңіз ¬p.[1] Бұл ұсынысты айтады б кез келген кейінгі өңдеу кезінде «дұрыс емес» деп қабылданады. Алайда, жоспарлаушы логикалық модельге негізделмеген, алдыңғы логикалық интерпретация түсініксіз болып қалады.

Пролог семантикасы

Форманың таза Prolog, NAF литералдары сөйлемдер денесінде болуы мүмкін және басқа NAF литералдарын шығару үшін қолданыла алады. Мысалы, тек төрт тармақ берілген

NAF туындайды , және .

Аяқтау семантикасы

NAF семантикасы 1978 жылға дейін ашық мәселе болып қала берді Кит Кларк логикалық бағдарламаның аяқталуына қатысты дұрыс екенін көрсетті, мұнда еркін түрде «тек» және «iff» немесе «түрінде жазылады» деп түсіндіріледі".

Мысалы, жоғарыдағы төрт тармақтың аяқталуы

NAF тұжырым ережесі эквиваленттіліктің екі жағын да жоққа шығарып, оң жағындағы терістеуді төменге қарай тарататын аяқталғанға дейін нақты дәлелдеуді модельдейді. атомдық формулалар. Мысалы, көрсету , NAF эквиваленттермен ойлауды модельдейді

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

т

NAF туындайды .

Бағдарламаның аяқталуы

аксиомалар мен домендерді жабу аксиомаларының ерекше атауларымен толықтырылды.

Аяқтау семантикасы екеуімен де тығыз байланысты айналма жазба және жабық әлемдік болжам.

Автоэпистемалық семантика

Аяқтау семантикасы нәтижені түсіндіруге негізделген классикалық теріске шығару ретінде NAF тұжырымының туралы . Алайда, 1987 ж. Майкл Гельфонд түсіндіруге болатындығын көрсетті сөзбе-сөз « «,» көрсету мүмкін емес «немесе» белгісіз сенбейді », сияқты автоэпистемикалық логика. Автоэпистемиялық интерпретацияны әрі қарай Гельфонд және Лифшитц 1988 ж. және негізі болып табылады жауаптар жиынтығын бағдарламалау.

NAF литералдары бар таза Prolog P бағдарламасының аутоэпистемика семантикасы P-ны «өзгертусіз» NAF литералдар жиынтығымен «кеңейту» арқылы алынады, яғни тұрақты деген мағынада

Δ = { | P мағынасын білдірмейді ∪ Δ}

Басқаша айтқанда, көрсетілмейтін нәрселер туралы жорамалдар жиынтығы тұрақты егер тек Δ болса, онда P бағдарламасынан шынымен көрсетілмейтін барлық сөйлемдердің жиынтығы Δ -ге кеңейтілген. Мұнда таза Prolog бағдарламаларының қарапайым синтаксисі болғандықтан, «тұспалдап» тек қарапайым модондар мен әмбебап инстанцияны қолданатын туынды деп түсінуге болады.

Бағдарламаның нөлдік, бір немесе бірнеше тұрақты кеңеюі болуы мүмкін. Мысалға,

тұрақты кеңеюі жоқ.

дәл бір тұрақты кеңеюге ие Δ = {}

тура екі тұрақты кеңеюге ие Δ1 = {} және Δ2 = {}.

NAF-тің автоэпистемалық интерпретациясын кеңейтілген логикалық бағдарламалаудағыдай және классикалық терістеумен біріктіруге болады жауаптар жиынтығын бағдарламалау. Екі терістеуді біріктіре отырып, мысалы, білдіруге болады

(жабық әлемдік болжам) және
( әдепкі бойынша ұсталады).

Сілтемелер

  1. ^ Кларк, Кит (1978). Логика және мәліметтер негіздері (PDF). Шпрингер-Верлаг. 293–322 бб. (Терістеу сәтсіздік ретінде). дои:10.1007/978-1-4684-3384-5_11.

Әдебиеттер тізімі

Сыртқы сілтемелер

  • Есеп беру өзара әрекеттесу үшін ережелер тілдері бойынша W3C семинарынан. NAF және SNAF туралы ескертулерді қамтиды (ауқымды терістеу сәтсіздік ретінде).