Математическая логика. Шапорев С.Д (1019113), страница 31
Текст из файла (страница 31)
—— в. Шаг 2. Если Р, — одноэлементнсе множество, то конец алгоритма, НОУ=Ог . В противном случае накодиьз множество рассогласований В». Шаг 3. Если В, не содержит переменных, ю конец «лгоритма, множество исходных формул не унифицируемо. Если В, содержит переменную х, и терм г, несла х входит в г,,то конец алгоритма, множество литералов не унифицнруемо. Шаг 4. Если сушествуег х,,тз б Т такие, по х„— переменная„не вхоляшая в гг, то О = )гг(гг ), Ог — — Ог О=От (гя(хг)и Ргм =Ря(гг(хг)= РяО или Рам = Рйг .
Шагу й = й ь П переход на начало второго шага. Если количество литералов больше двух, ю последовательно уиифицнруется первый со вторьяя литералом, затем резуш тат унификации унифицнруетс» с треп им литералом и так далее до тех пор, пока либо все ьзножество литералов нс будет унифицировано, либо получен ответ о том, что это множества не унифнцируемо. Теорема йр Если Є— конечное иепустое упмфмняруемое множество атомарных формул, то алгоритм унификации всегда заканчивает работу па втором шаге и последиаи подстановка Ол будет ПОУ для Р,.
Пример Е Рс = (Р(х, Т(у, й(п)), й(х)), Р(х, Т" (у, х), у)). Шаг й Е=О, Є— исходно«множество,О =я. Шаг 2 Ре — неодноэлемшпное множество, Ве — — (й(а)х). Глвва 4 Ис гисление о диквюв Шагу хй 1(а). Шаг 4 х — перемсннав, д(а) — -терм, х не вводите д(а), О = (5(а)х) В, = О 0 = (д(а)х] Р, = РВ, =51Р(5(а))(у,д(а))1г(д(а)))Р(д(а)/(у,д(а))у)).
Шаг 5. Ь' = 1, переход на второй швг. швг 2 Р, — неодноэлемснтное множество, уэ~ = (ь(д(а)) у) Шаг 3. УК 1г(Д(а)). Швг4 0= 10(0(а))у) О =0~0= м( ) ' (, ( ) Рэ = 10г = (Р(0(гг) У (Ь(0(а)) 0(а))Ь(0(а)))Р(0(а)г(Ь(Ь(а)) 0(а)) !г(0 (а)))) = (Р(0 (а)/(Ь(д(а)) 0(а)) Ь (д(а)))). Шаг 5. Ь = 2, переход на второй швг. Ша~ 2.
Рэ — одноэлемеитное множество, конец алгоритма НОУ = Вэ — — (0(а!л,1г(д(а))у). Пример 2. Рв =ЗР(хх (и, дд(к)1г(гг))) Р(х, Г(а,и,"))). Швг 1. Ь = О, Ре — исходное множество. Ог —— к Шаг 2. Рв — неодноэвс мент псе многие ство, !ус = к5 (к) и) Шаг!. ий д(к) шв 4 0=(0(х)гг),0, =ВОВ=Ь(к)гг), Р, = РО, = ЗР(х,! (а 0(х) Ь(д(4)) Р(х у(а40(к)) 2)) Швг 5. Ь = 1, перевод на второй шаг. Шаг 2 Р, — неодиоэлементиос множество, ЗЗ, = у' (0( )), к).
1!!вг 3. гн Ь(д(к)), конец шггоритма, множество Р„нс унифицируемо. часы! маюмвгимск ял и ля гп4 4.9. Метод резолюций в исчислении предикатов Метод резолюций уже рассчатриватся нами в разделе 2.7. Его практическое использование в исчислении предикатов значительно сложнее, чем в исчислении высказываний. Теоретическая основа метода не изменилась. Для того чтобы доказать, что из некоторою множества формул исчисления предикатов логически слелует данная формула, берут отрицание этой формулы и добавляют ее к исходному множеству. После чего доказывают противоречивость формулы, являющейся «оньюнкцией формул исходного множества н данной.
По существу, зто не что иное, как метод докюательства от противного. В отличие ат исчисления высказываний в исчислении предикатов в методе резолюций есть особенности. Для исклгочения кванторов исходное множество форыул необходимо приводить к У-форме и унифицировать. После тато как получено множество дизьюнктов, осуществляеюя процесс опровержения, внвлогичныд исчислению высказываний: на каждом элементарном шаге доказательства используе1ся правило, называемое ргзолюяиеб.
Основная идея метода состоит в следующем. Для тою чтобы доказать, что формула А логически следует из некоторого множества формул Г=~дпА1,...,А„~, нужно доказать, что множество форьгул Г1 иГь)ТА) противоречиво, т. е не существует интерпретации, в которой бы оно удовлетворялось. Множество Г, противоречиво тогда и только иногда, когда формула А, лА, л... лА. — 1 А является сбщезначимоя, т.е. истинной в любой интерпретации. Для того чтобы определить интерпрещцию мнозмства формул, необходима задать область интерпретации. Однако таких областей для формул исчисления предикатов мажет быть бесконечно иного. Чаще всего в качестю области интерпретации берут множество Н, нюываемоеуниеерсумом Эрбрала . уеоргма 4)0 Если мимкество формул Г неудовлетворимо на Нг, то оно неудовлетворимо ма любой другой областя интерпретации.
Универсум Эрбрана рекурсивиа строится следующим образом, 1. Множество всех предметных констант из Г приныыежит Н„. Если Г не содержит ни одной предметной констаитм, то в Нг входнт произвольная предметна» констакпь называеиая любым именем. Жв Эрбр ()90В-1931) — фмянузскяв аге м Тляяа 4 И и пени л дика в 2 Если термы г, б Н А=1,и и 1, — какой-нибудь функциональный символ, зависащий от н пеРеменных, и 1", и Г то 1,(г,,гз,,г„) и и, папРнмеР ! = Т(х)о Як у) Р(Г(х)Р(1(х))у Я(0(и)))), Н г =(з1 (и) В(п) 1(1 (и)) /(Д(а)) Д(! (и)) Р(б(а))...), Г = ~~/ (си Р(с)2(сз)2Р(с ) Р(х х 1(х))Р(х у, )и Рз(х з)Р х)ч ч Р(ухп)ч Рз(хи)ч Рз(хз) Рз(си с,)), Н =~,,с„сзь1(с,)((сз)1'(сз) 1(!'(с,)) ..) Метод резолюций основывается на теореме Зрбрана.
Теоусмо 4.11 1меорел а Эрбрапа1. Множесгво анзыонктов Г иеиыполив. мо тогда и тольюз тогда, когда вместе» конечмое невыполнимое множество Гг константных частных случаен зтихднзъювктов иа Н,. Таким обрезом, мнохщство Г невыполнимо, если можно найгн такис подстановки констант из Нг вместо предметных неременныщ прн которых полученное множество дизъюиктов будет противоречивыч.
Пусть  — лизъюнкт сигнатуры Х вида В= А, у А, у...уЛ, уС нлн В = А, чА» у.,ч А„уС, где А, — атомарныс формулы. Предполозким, гю множество (А,,Аы,..,А„) имеет ПОУ О, Тогда А~О>, у СОл или А!Ор у СО~ называется склейкой В, Пусть В, а В, — дяа дизъюнкга, не имеющие общих переменных, Л, и ~ — атомарные формуяы или атринания атомарных формул я В, и В, Если А, и А, имыог ПОУ Ор, то лизыонкт, получаеиый пз бюрмуззы В,йе Взбе яычеркиианчем А,О, и Азйг, называется бипсрюг! Резозызептой В, и В„а формулы А, и Аз — оигрсзоемынп. Если В,Ог — — А, и ВзОр = Аз,то бинарная резсльвента В, и В, равна нулю Если формулы В, и Вз яме~от общие переменныс, то перел нахождением их бинарной резольвенты в одной из формул общие переменные надо переименоват~ Пример !.
В, =1',(т)чР (хс), В =Р(сз)кР (с„г). Формулы В, и В, общих пораненных не имеют. Пусть А = Р (х), А, = Р (сз), А = Р (с), 0 = Цх), Чаев ! Магамапжаскаялеика В Оч В О = Р»(с»)о Р (с,,с ) » Р(с )ч Р (с„с ). Так как А О = Р (с» ), А О = Р (с» ) вычсркнем ик Тогда бинарная рсзольвснта В, и В» равна Р,(с„с,). Рсзольвентой дизъюнктов В, и В» гез(В„В,) нззывастся одна из слсдующнх: Б Бинарная рсзольвснта В, и В . 2. Бинарная рсзольвснта склейки В, и В,. 3.
Бинарная рсюльаснта В, и скясйки В». 4. Бинарная резольвснта сктсйки В, и сквсйки В. Пример 2. Найти всс возможныс резолыщнты следующего множсства формул )Р (х,з)о Р»(х) Р (х т)ч Рз(с) Р»(с) Р»(х)сР»(х) Р (х ~(х))). Пусть В, = Р~х т ч Р (с), В, = Р (х У(х)), А, = Р (х с), А, = Р(х,~(х)), А, =Р(х,/(х)), О= ~Е(х)с), В О ч ВО = Р (х ) (х)) ч Р (с) ч Р (х ~ (х)) Бинарная рсзольвснта В, и В, равна Р,(с), газ(ВпВ,)= Р»(с). Аналогично пусть В = Р (х т) .
Р (с), В» = Р»(х)чу»»(х), »~ = Р» (с), А, = Р» (х), А = Р»(х), О = Щ, В»йоВ О = Р(с,с)ч Р (с)ч Р»(с)о Р (с), пи(ВпВ»)= Р,(с,с)оР»(с) Пусть à — множсстволизъюнктов. Резолютивный вывод С из Г ость такая оослсдомпсльность фѻ,...,С, дизъюнктоа, что С=С„и каждый днзь- юнкт С, или принадлежит Г, или является рсзольвснтой дизъюнктов, пред- шастяующик С, . Как уже упоминалось, »ща докамкльства выводимасти С из Г можно пока»ать, что множестю Г» = Г щ (С) явяяюся противорсчивым.
Этот способ докззатсльства основывастся иа слсдующсй теорсмс. Гла а 4 Исчисление л ияагое лог Уеореиа 4 ей (а яоааолзе жюлодо Резоеюнлйй Если à — множество дпзьюиктоа, то множество замыканий всеобщности формул нз Г невыполнимо тогда и только твгла, когда существует рсзолютннвый вывод муля нз Г. Примеру. Проверить на противоречивость следующее мнтвкссгво формул; Г= (Р(с~ Рз(у)ч Р(с„у)Р(х) г РЯу)ч Рз(х у)Рз(сз) Рз(сг)) Ж Рз Рз Рг Рз) В, = Р,, Вз =Рз, А, =Р,(с,), А, =-Р,(х), 8=(сД ВОч Взй = Р(с)ч Р(с)ч Р(у)ч Рз(с„у), Ре = гез(Роуз)= Рт(у)чРз(с~ У)' В, = Р., Вз = Ры А, = Р (с„у) ~ ы Р (с,, у) 8 = е, ВйчВзО=Р(с,,у)чрз(у)чР(у)чр(с„у), Г = гас(Гз,Ра)ы Р,(у)ч РЯу); В~ = Ре Вз = Г,, А~ = Рз(сз ) Аз ы Рз(у) О = Иу), Вйч Вз8=Рз(сз)чРз(сз)ч Р(сз), Р; = гсз(Р„Г)= Р(сз); гсз(Гз,ут)= гез(Р (сз)Р(сз))=0.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
