Математическая логика. Шапорев С.Д (1019113), страница 30
Текст из файла (страница 30)
Для исчисления предикатов занятие эк- вива»еитности формул в их дедуктивной эквивзлентнссти не равнозначно. Т»арамо 4К Если 6 и Г эквивалентны в исчнслсини преднкатогъ то оии н дедуктивно эквивалентны. Докозлжгльслмо Глава 4. Исчисление л еди»аюа гаг рема Е9), поэтому либо формула исчисления вьюказывы|ий выводима, либо Ее присоединение к аксиомам исчисления ведет к противоречию. Если две формулы исчисиения высказываний выводимы, то оии просто эквииаынтны бали жа одна выводим», а другая нет, то они ие могут бьггь делуктивно эквивалентными, т.
к. присоединение выводимых формул к аксиомам исчисления Новых выводимых формул ие дает, поэтому друга» невыводима» формула астансгся невыводимой. В заключение без доказательства привадем две практически важные теоремы исчисления. Теорема 4. 7 Люба» выводима» в исчислении преднкатав формула обще- »и»чиню Теорема 4.8 (меорема Геделя ).
Всяка» тождественно астнанан формуле логики предика»он ивлветс» выводнмой в исчислении иреднкатоа. 4. 4. Получение д-формул. Скулемовокие функции Как уже упоминалссь в рпздгхе 3.6, существуют Ч-формулы, 3-формулы и скулемовские нормальные формы (»3-формулы). '4-формулы и скулемовскне норм»явные формы используются в методе резолюний исчисления предикатов.
Пусть формула сигнатуры Е имеет вид зрхфхз...)гх„йу)йуз...ЗУ»,А(хихз,...,хе, ум уэ,...уи), (4Л.!) где А(х,,хз,...,х„,у„у,...у„) — бескванторная форыула. Покажем, носу. нмствуют ~„Дз,...,Т вЂ” н-местные функнионатьные символы, не входящие в сигиатуру Е, такие, что для сигнатуры Е' =Е~ ~(ГИ Г„..., Г ) справедливо ( Кгх!))хэ- Кгх»ВУДуз..ЗУ»А(хмхз,,хь, ум уз, у,„) ьч +4 А(хпхз,,»„,Я(хг,хэ,,х„), Тз(хмх„...,х„)„., г,„(х„х„...,х„)). Лейатвитсльно, раасмотрим некоторый набор (а„а„,...,а„)п М, тле М— область определеии» предиката А . Если для этого набора )-ЗУ,Зуз ЗУ„А(а,,аз,...,а„, у„ у„...у ), та в качестве Е (а„ а„...,а„) Кургарилриягеяав(!904-!97») — н и а »юсиа Часть Г, Мвгем пмескля лепта гдя возьмем такие значения Ь,, что ~ — А(с„а„...,а„,Ь„Ь„...Ь,„). Если же ~РЗУ,Зуэ Зу„А(а„а„..„а„,у„у„...у ), то в «ачестяе /,(и„ат,...,а„) могкно взять произвольные значения.
Рассмотрим теперь более общий случай Зх, Зхь фу, (гу„ЗМ...Зги фииьфгг„Зэи.. (4.7.2) Поставим в соответствие каэшой переменной, связанной квантором сущест- вования, какую-нибудь функцию, опрелеленную на М, принимающую зна- чения из М и зависящую только от переменных, связанных кваитором вс»- общности и предшествующих данному квантору сущютвования. Если квантор существования стоит первым, то поставим ему в соответствие какое- нибудь значение переменной из области М . Дл» рассматриваемой формулы (4.7.2) переменным х, будут поставлены в соотнеютвие константм х,, перес менным М вЂ” фУнкции ),(У,,Уз,..., У„) и т.д., пеРеменным т, — фУнкции фг(у~ уэ -"у, .иыиз,...,иь ), Если эти константы н функции таковы, что в результате замены ими соотвюствующик переменных в предикате А(х~ - у,,...,х„...,и„...,г'„...) полученный предикат А(х,,„.,х„,уи, „у,)(у, у ),,~ (у, у ) и, и ф,(у„...,у„,и, и„),...,фь (Уи.,.,У„,и,,,и„)), та используемые константы и функпии х,,...,х„,у,(у,,...,у„), /„(уи...,у„) ф, (у,,..., у„,и,,...,и„),..., ф„, (Уг -.
У,, *из ",, ) называются рюрсшаюмими функциями или (ьуикчыми скулелги для форму- лы (4.7.2). Приведем несколько примеров. Пример 1. Рассмотрим следующую замюгугую предюрегэиую форму В = ЗхзУУЗх(ЗиЗэг(жА(х, у,х,и,э,ж). Обозначим значение х, когорос суэзесщует в соответствии с первым кваигором, консмнтой а, отбросив при этом квантор существования: В = тГУЗздгиЗэз(юд(и,у,з,и,э,и) тракт, что для всякого у может быть найдено значение дл» з, может быль выражен некоторой функцией х = 7"(у). тогда В ь фуфиЗээжА(и,у,у(у)и,э,ж). Глаш 4 Исчисление вр дикагов Уса Аналогично, тот факт, что лля любых у,и найлегся у, можно вьурвзить скулемовской функцией и = ф(у,и), которая подсташуяется вместо и В=туутУитунА(с,у<Р(у)уу,ф(у,уу)ж) Так как все переменные в исходной формуле должны быль связаны, кванторы существования исключены, а порядок кванторов всеобщности не влияег иа значение формульу.
то кванторы всеобшнссти отбрасывакпся в предположении, что все оставшиеся переменные ими связаны тогда В= А(а,у.у(у) н,ф(у н)ут), где а, у(у) и ур(у,н)— скулемовские функции. и!унмср ЗВля формулы уухзазуули((у > а — з у > х) у (и < ь) л (и < т)) построить ЗУ -формулу.
Здесь формула дана в конкретном виде и разрешауошие функции тоже могут быть выражены конкретно Коуукрсгизируем лишь область определения основного предиката Пусть М = РУ. Пололуим Х = уу(х) тогда УУз !Ууууу((у > Яу(т) — ь у > х)л(н < 1; (.т))л (и < х)). Анвлоюучно и = 1;(х,!) и зухтуу((у > уу(х) — г у> х)л(л(х,у)< Уу(х))л~Ят,у)<.г)) Осталось подобраш вид фууукууий у", и уг таким обрюом, чтобы формУла (У>ту(х) — ь У>х)л(Уз(х,У)< Уу(х))л(Уз(х,У)< ь) была бы истинной при любых х,уи АУ. Например, можно взять у (т)= т+1, а Уз(х)=л.Тогда (У>хч.1 — ь У>х)А(У<к+1)л(л<х)н Ул1л1н! Пример б.
Дда формулы УухУУуЛлбг(Р(хг)л Р(у,з)) построить УУ- формулу. Пусть М = (01). х= уу(х,у), ЬухтууЗу(Р(х, у)л Р(уу;(ху))), У= ут(х,у), гухгуу(Р(х,уз(х,у))л Р(у!у(х,у))). Здесь Р— любой диухместный преликат, позтому функции Уу и у; необходимо выбрать так, чтобы формула Р(х, !' (х, у))о Р(у, Т, (х, у)) была тождественно невинной Положим Ру(х,у)=у (х,у)=1, причем пусть Р(хО)=1 и Р(х,1) = 1.
Тогда Р(т, /, (х, т )) у. Р(т 3 у (х у)) = Р(х !) л Р(у 1) =-! л 1 и ! Часп Г. Маты тыкмаялмияе Примерд. згхзгуйгйвчг(5(ху у)-э(5(ггх)лР(тг4)), М =Дз 5(х,у,г)=(хе у=в), Р(х,у,г)=(х у= в). Пусть г = У, (х, у), г = У (х, у), тогда згх0уьгтг5(х, у, у) — з (5(Я (х, у) Уз (х, у) х) л Р(Уз (х, у) г,г))). (х -1,х > О, Выбезюм г=у";(х,у)= в «=уз(х,у)=1,тогда О,х=О, 5(х,у,у)е(5(У(х,у) уз(х,у)х)лР(у,(х,у)гг))м (хе у= у)-э — э((х-1т1=х)л(1 с=с))=(хе у = у) — +1л! — 1. 4.8. Унификация формул исчисления предикатов Для получения подходящих резольвент в методе резолюций исчисления преднктгов применякпся полствиовки в формулы исчисления.
Процесс этих подстановок называется улификснкей. Псдсмалоекой сигнатуры Х называется «онечнсе множество вила Цхз,гз/хз,...,г,/х„1 или ((г„х, )(тз,хз)...,(г.,х„)), тле г, — терм сигнатУ- ры Е, отличный ог х, (1 <! < л), а все переменные х„хз,...,х„различны. Подстановка, которая не солержит элементов, называется густой и сбозначытся в . Осли дана подстановка 0 = (5(гйх,а)у1, та 5(г1х означает, что повсюду переменная х звменяегс» функцией 5(г), а переменная у — предметной коиствнтой а. Пусть имеею» атомарная формула (литерал) Р(х,у,г). Булем обозначать через РО частный случай литерала Р, получающийся при использовании подстановки О.
Результат применения подстановки 0 к кажламу из литералов множества литералов обозначим (Р~ 10 . Определим композицию двух нли нескольких подстановок. Пусть О = 1г,/хз,тз!хз„,г„!хе 1, Х =(Оз!ус йз!у„.,й„!у„) — подстановки сигнатуры Х, Тогда композиция ОХ получаезс» из множества (г Х~хз, гзХ~хз,..., Г„Х~х„, д ~ У,, От~Уз,..., де ~Ум ) вычеРкиванием всех элементов с Х)х, для которых г Х=х, и всех элементов д,~у, таких, что з 1 з /Левал.и чк л ~и дккагое у, ц (х„х„...,х„) Например, пусть О = (Р(у,г)х,г(у)= (г/хит /хз), Х=(л~х,Ь~У,с~Р гав) (Ч~!У~ От~Уз ба~Уз,ба~Ус) 'тогда (Г,Х)хи ГзХ)хз, Чз)уз, ЧДУз, Ч4уз, Че(уа)и Нб,с1х4У4х Ь) У,4а,б~тс) Здесь гХ=У(Ь с)мх=х,, ГзХ=сц у=аз У, =«ц(х У).
Уз =Уц(г У), у, =ай (х у), у, = мй (х у). Следовательно, вычеркнуть надо а~х и с(у, тогда композиция двух подстанавок 9Х будет иметь вид (У(Ь,с)х,с(у,фтОж) Дпя подстановок справедливо следующае. й (РО)~; = РОь, т.е. послеловательное применение подстановки 8, а затем постановка Х приводит к тому же результату, что и применение композиции подстановак. 2. (ОЛ)5 = 0(20), т. е. композиция подстановок ассоциативн~ Подстановка О сигнатуры Х называется улификамораи для множества (А„А,...,А„) формул сигнатуры, если тдО=~О=...=А„О. Множество формул (А„Аз,...,А„) сигнатуры Х называется улирзихирусимлг, если для него существует уннфикатор. Наиболее общим нли прзстемлии увификллюрам ~НОУ) для множества формул (А,,Аз,...,А„) называется унификатор Ор, «слн лля любого другого унификатора 8 существует подстановка 8, такая, что 0 = Олб,.
Существует алгоритм, называемый аагорылмом улигдлкпхии, который приводит к наиболее общему унификатору для унифицируемого множества (ть,дз,...,А„) или Фюбщает о невозможности зто сделать, «сли множество формул не уинфицируеью. Пусть (А„А„,.„А„) — непустсе множества атомарных формул сигнатуры Е. ДУлолгесюеом рссссглссоелнии в (А,,~,...,А„) казываетсв множество отличающихся тернов в первой слева позиции. Наприлгер, для множества (Р(т, у (у, З(л)) Ь(х)) Р(х, У(у, х), у)) множеством рассогласований «вляется (б(а),х): в первой слева позиции первого литерала стоит терм д(л), который отличается от соответствующей тпервой слева) позиции второго литерала х.
Ча гь Г Мя емяпмесяая лап «а для множества (Р(х, г(у,г))Р(х,е)Р(х,Т(у,~,(г)))) множество рассогласований — () (у,я)с, г (у,~(Г))) (подчеркнутьг в основном множестве формул). рассмотрим алгоритм унификации для двух литералов. На каждом шаге алгоритма подстановка применяется к каждому пз литералов. Пусть Є— нсхолнсе вепустое множество атомарных формул, Ое = с — пустая подстановка, Обозначим на й-и шаге: Р, — множество атомарных формул бзитералов),  — множество рассогласованпй, Ог, — осуществляемая подстановка. Приведем шаги алгоритма унификации для двух литералов. Шаг й =О, Рг = Рс, Ог.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
