МАТЕМАТИЧЕСКАЯ ЛОГИКА И ЛОГИЧЕСКОЕ ПРОГРАММИРОВАНИЕ. Литература. 1. Клини. Математическая логика. 2. Мендельсон. Введение в математическую логику. 3. Чень, Ли. Математическая логика и автоматическое доказа- тельство теорем. 4. Логика и компьютер (сборник под ред. Смирнова). 5. Братко. Программирование на языке ПРОЛОГ для искусственно- го интеллекта. 6. Логическое программирование (сборник по ред. Агафонова). 7. J.W.Lloyd. Foundations of Logic Programming, 1987. План лекций. Часть I. Математическая логика. $1. Язык логики предикатов. Синтаксис языка логики предикатов: алфавит; термы; формулы. Алфа- вит языка представляет собой объединение алфавитов: 1) переменных (предметных); 2) функциональных символов; 3) предикатных символов; 4) логических связок (конъюнкция &, дизъюнкция V, импликация >, отрицание ї); 4) кванторов (квантор общности A., квантор существования E.); 5) вспомогательных символов (скобки и запятые). Каждому предикатному и функциональному символу сопоставлено число n>=0, называемое его мест- ностью. Терм - это переменная или выражение f(t1,...,tn), где f - n-местный функциональный символ, а t1,...,tn - термы. Формула A - это выражение P(t1,...,tn), где P - n-местный предикатный символ, а t1,...,tn - термы, или выражение, построенное из других формул с при- менением логической связки или квантора: їC, (C&B), (CVB), (C>B), A.x С, E.x C, где B и C - формулы, а x - переменная. Эта логическая связка (квантор) называется главной (или внешней) связкой формулы A. Понятия, описывающие кванторную структуру формулы: пусть Q - квантор; подформула B формулы QxB называется областью действия кванто- ра Q по переменной x; переменная x называется свободной в формуле C, если не входит в область действия никакого квантора по x; в формуле QxB квантор Q связывает все свободные вхождения переменной x в формулу B. Формула называется замкнутой, если содержит только связанные вхож- дения переменных. Семантика языка логики предикатов: интерпретация; истинность в интерпретации формулы B(x1,...,xn) со свободными переменными x1,...,xn на наборе b1,...,bn (запись I|=B[b1,...,bn] означает, что в интерпре- тации I формула B истинна, если каждая ее свободная переменная xi при- нимает значение bi). Интерпретация I - это, во-первых, некоторое множество D, называе- мое областью интерпретации; во-вторых, множество всюду определенных n-местных функций f^ из D в D, сопоставленных n-местным функциональным символам f; и в-третьих, множество всюду определенных n-местных функ- ций P^ из D в множество истинностных значений {истина,ложь}, сопостав- ленных n-местным предикатным символам Р. После того, как эти три мно- жества зафиксированы, значения термов и формул в I определяются следу- ющим образом. Пусть x1,...,xn - список переменных, содержащий все пе- ременные терма t, а b1,...,bn - элементы D. Значение t на наборе b1,...,bn определяется так: если t есть переменная xi, то xi[b1,...,bn] = bi; если t имеет вид f(...,tj,...), то f(...,tj,...)[b1,...,bn] = f^(...,tj[b1,...,bn],...). (Т.е. каждый терм интерпретируется как сложная функция из D в D). Пусть x1,...,xn - список переменных, содержащий все свободные переменные формулы B, а b1,...,bn - элементы D. Формула В истинна в интерпретации I на наборе b1,...,bn (I|=B[b1,...,bn]) в следующих случаях. Если B есть P(...,ti,...), то I|=B[b1,...,bn] <=> P^(...,ti[b1,...bn],...)=истина. Если В есть їA, то I|=B[b1,...,bn] <=> не верно, что I|= A[b1,...,bn]. Если В есть A&C (AVC), то I|=B[b1,...,bn] <=> I|= A[b1,...,bn] и (или) I|= С[b1,...,bn]. Если В есть A>C, то I|=B[b1,...,bn] <=> из I|= A[b1,...,bn] следует I|= С[b1,...,bn] (т.е. не верно, что I|= A[b1,...,bn] или I|= С[b1,...,bn]). Если В есть A.xC (E.xC), то I|=B[b1,...,bn] <=> для любого (какого-то) b0 формула С(x0,x1,...,xn) истинна в I на наборе b0,b1,...,bn: I|= C[b0,b1,...,bn]. Таким обра- зом, каждая формула B интерпретируется как сложная функция из D в мно- жество {истина,ложь}. Замечания: 1) область интерпретации выбирается произвольно, пре- дикатные и функциональные символы интерпретируются в каждой интерпре- тации по-разному, а логические связки и кванторы интерпретируются всегда одинаково (причем логические связки - в соответствии с истин- ностными таблицами); 2) истинностные значения формул A.xB и E.xB не зависят от значения x; 3) в каждой интерпретации формула со свободными переменными представляет собой истинностную функцию от этих пременных, а замкнутая формула принимает определенное истинностное значение; 4) определение семантики позволяет вычислять истинностные значения логи- ческих формул в конечных интерпретациях (делая это, можно, в частнос- ти, убедиться в адекватности формальной семантики: интуитивное и фор- мальное истинностные значения большинства формул совпадают); 5) в со- держательной математике обычно используются определенным образом про- интерпретированные варианты языка логики предикатов, а в математичес- кой логике рассматриваются произвольные интерпретации каждого языка; 6) если в интерпретации I формула В не зависит существенно от перемен- ной x, то истинностные значения формул В, A.xB и E.xB совпадают. Ясно, что 0-местная функция - это константа. Вопрос: что такое 0-местный предикат? С учетом определения семантики, это выражение, принимающее ровно одно из значений истина/ложь в каждой данной интерп- ретации (в отличие от логических констант T - "истина" и Б - "ложь", принимающих соответствующие истинностные значения во всех интерпрета- циях). Такие предикаты можно рассматривать как пропозициональные пере- менные, принимающие значения из множества {истина,ложь}. Если рассмат- ривать только 0-местные предикаты, язык логики предикатов превращается в язык логики высказываний (т.к. в 0-местных предикатах нет "мест" для термов, оказываются избыточными алфавиты переменных и функциональных символов, а в силу зам.6 бесполезны кванторы). В языке остаются пропо- зициональные переменные и логические связки. Поэтому семантика языка логики высказываний может быть полностью определена в терминах истин- ностных таблиц. Каждая строка таблицы соответствует одной интерпрета- ции, а таблица в целом - совокупности всех интерпретаций (следователь- но, их число конечно). Итак, истинность формулы со свободными переменными в каждой ин- терпретации зависит от значений ее свободных переменных. Такое понима- ние истинности логических формул соответствует "истинностному смыслу" строгих определений (определение - это логическое суждение, истинное на множестве определяемых объектов); "истинностному смыслу" уравнений, рассматриваемых как логические формулы (формула, состоящая из двух термов, соединенных знаком "=", называется уравнением, если стоит воп- рос: при каких значениях переменных это равенство имеет место), и т.п. Замкнутые формулы соответствуют аксиомам, теоремам, тождествам (т.е. различным логическим суждениям). Иногда содержательные суждения (как в формульном, так и словесном виде) записываются без кванторов (квантор- ных слов), но при этом подразумевается, что они истинны во всей облас- ти интерпретации (тождества, правила). Такому пониманию формулы B со свободными переменными x1,...,xn соответствует обозначение I |= B (формула B истинна в интерпретации I), означающее, что формула В ис- тинна в I при любых значениях переменных x1,...xn на множестве D (I|=B[b1,...,bn] при любых b1,...bn). Моделью (контрпримером) формулы A называется интерпретация, в ко- торой A истинна (ложна). Модель/контрпример множества формул - это мо- дель/контрпример конъюнкции этих формул. Нетрудно проверить, что с точки зрения семантики логики предика- тов аксиомы математических теорий (например, евклидовой геометрии) ис- тинны не во всех интерпретациях: они имеют модели, но к ним можно построить контрпримеры. Бывают ли формулы, истинные всегда (не имеющие контрпримеров)? Да, например, A > A: "из A следует A" (в этом можно убедиться, построив истинностную таблицу). Назовем их общезначимыми (обозначая |= A). Вопрос: представляют ли такие формулы какой-либо ин- терес с содержательной точки зрения? Введем понятие логического следо- вания: A|=B означает, что в любой интерпретации из истинности A следу- ет истинность B (при этом A1,...,An |= B понимается как A1&...&An|=B). Например, если A описывает совокупность аксиом некоторой математичес- кой теории, и в этой теории B - теорема, то их отношение можно запи- сать как A|=B. Т1 (теорема о дедукции). Если A и B - замкнутые формулы, то A|=B <=> |= A>B . Д. следует из определения логического следования и истин- ностной таблицы для импликации. Теорема о дедукции показывает, что доказательство теорем в содер- жательных теориях сводится к установлению общезначимости определенных формул. С другой стороны, в некоторых общезначимых формулах можно "уз- нать" схемы доказательств (от противного, разбор случаев, закон конт- рапозиции и др.). Таким образом, можно сказать, что общезначимая фор- мула - это определенная форма записи доказательства. Пусть x1,...,xn - все свободные переменные формулы B. Тогда A.B обозначает результат замыкания B кванторами общности, т.е. формулу A.x1...A.xn B. Т2. При замыкании формул кванторами общности сохраняется логичес- кое следование (B|=C <=> A.B|=A.C). Д. следует из определений логичес- кого следования и отношения I|=B. Замечание. Для незамкнутых формул Т1, вообще говоря, не верна. Ее правильное применение требует предварительного замыкания этих формул кванторами общности. Ключевые слова к $1: предикат, терм, формула, подформула, атом=атомарная/элементарная формула, логическая связка, главная=внеш- няя связка формулы, квантор, свободное/связанное вхождение переменной, замкнутая формула, интерпретация, модель, контрпример, пропозициональ- ная переменная, истинностная таблица, логическое следование, общезна- чимость, общезначимая формула, язык логики предикатов/высказываний. $2. Исчисление натурального вывода (N-исчисление). Правила натурального (естественного) вывода моделируют элементар- ные приемы, используемые в содержательных доказательствах. Натуральный вывод отличется от содержательного доказательства: 1) большей подроб- ностью; 2) явным упоминанием всех предположений (гипотез), в том числе - аксиом и теорем математической теории, в которой выполняется доказа- тельство; 3) явным выделением понятия "исключаемых" в процессе вывода гипотез; 4) фиксированным множеством правил вывода. Вывод - это дре- весная конструкция, построенная из формул по правилам вывода (в корне дерева располагается выводимая формула, а в листьях - гипотезы). Неко- торые правила, по определению, исключают гипотезы: посылка правила считается зависящей от соответствующей гипотезы, а заключение - нет. Формула A называется выводимой в исчислении N (обознается: |-N A), ес- ли можно построить такой ее вывод, в котором исключаются все гипотезы. Знание правил вывода дает возможность отличить правильно построенный вывод от неправильного, но (вообще говоря) не помогает строить выводы. Для этого нужны правила поиска вывода, которые описывают переход от одного (незавершенного) фрагмента вывода к другому и позволяют, начав с выводимой формулы, построить весь вывод. Ниже перечислены правила НАТУРАЛЬНОГО ВЫВОДА (формулы над чертой называются посылками правила, а формула под чертой - его заключением; буква i в названии правила означает, что применение правила вводит ло- гическую связку или квантор, а буква e - что уничтожает; в квадратных скобках над одной из посылок правила указан вид исключаемых этим пра- вилом гипотез). Конъюнкция: F1 F2 F1 & F2 F1 & F2 &i ------- &e1 ------- &e2 ------- F1 & F2 F1 F2 Дизъюнкция: [їF1] [їF2] [F1] [F2] F1 F2 Б F1VF2 F3 F3 Vi1 ------- Vi2 ------- Vi3 ------- Ve ---------------- F1 V F2 F1 V F2 F1 V F2 F3 Импликация: [F1] [їF3] [F2] F2 F1>F2 F1 F1>F2 F1 F3 >i ------- >e1(modus ponens) --------- >e2 ---------------- F1 > F2 F2 F3 Отрицание и ложь: [F] [їF] їF F Б Б Бi ----- їi --- їe --- Б їF F Кванторы: [(Svw)F] (Svw)F A.v F (Svt)F E.v F F1 Ai+ ------ Ae- ------ Ei- ------ Ee+ ----------- A.v F (Svt)F E.v F F1 Обозначения: (Sxy)F - подстановка: замена в формуле F переменной x на терм y; w - константа, не встречающаяся в заключениях правил Ee+ и Ai+ и в гипоте- зах, от которых эти заключения зависят; t - терм, свободный для v в F (терм t называется свободным для переменной v в формуле F, если пере- менная v cвободна в F, и при замене всех вхождений v на t ни одна пе- ременная из t не оказывается связанной); Правила ПОИСКА НАТУРАЛЬНОГО ВЫВОДА. Конъюнкция: Дизъюнкция: &ai |- F1&F2 => |-F1 / |-F2 Vai |- F1VF2 => їF1;їF2 |- Б &si F1; F2 => F1&F2 Vae F1VF2 |- F3 => F1|-F3 / F2|-F3 &se1 F1&F2 => F1 Vsi1 F1 => F1VF2 &se2 F1&F2 => F2 Vsi2 F2 => F1VF2 Импликация: Отрицание и ложь: >ai |- F1>F2 => F1|-F2 Бsi їF; F => Б >ae2 F1>F2|-F3 => їF3|-F1 / F2|-F3 Бdel Б |- F => >ae1 F1>F2 |-F2 => |-F1 їai |- їF => F |- Б >si F2 => F1>F2 їae1 |- F => їF |- Б >se1 F1>F2; F1 => F2 їae2 їF|- Б => |-F Кванторы: Aai+ |- A.vF => |- (Svw)F w - новая константа Ase- A.vF => (Svt)F t - терм, свободный для v Eai- |- E.vF => їE.vF |- (Svt)F в формуле F Esi- F => E.v (Stv)F ПОИСК НАТУРАЛЬНОГО ВЫВОДА формулы A. Основная идея: начиная с |- A, по обе стороны от знака |- добав- ляем формулы (в соответствии с правилами поиска вывода) до тех пор, пока не получится фрагмент A1,...,An |- An,An+1,...,Am, который можно заменить на вывод A1,...,An,An+1,...,Am. Правила поиска вывода делятся на аналитические (в названии кото- рых встречается буква a) и синтетические (с буквой s). Синтетическое правило имеет вид B1,...,Bn => B ( n>=1, в записи нет знака |-). Пра- вило применимо в том случае, когда в строящемся выводе слева от |- есть формулы B1,...,Bn (возможно, не подряд и в другом порядке). Ре- зультатом его применения является добавление формулы B слева от |- (в вертикальной записи - выше |-). Все остальное остается без изменений. Аналитическое правило имеет вид B1,...,Bn |-C => D1 |-E1 /... / Dm |-Em (n>=0, m>=1). В результате его применения на месте "старого" знака |- возникают подвыводы D1|-E1,...,Dm|-Em. В дальнейшем каждый из ------ ------ них достраивается отдельно (причем все формулы из объемлющих подвыво- дов, стоящие выше |-, считаются доступными в текущем подвыводе). Вывод считается построеным, если построены все его подвыводы. $3. Исчисление секвенций (G-исчисление). Формула, выводимая в натуральном исчислении, по определению, не зависит ни от каких гипотез, что означает возможность ее доказательст- ва безо всяких дополнительных предположений (например, аксиом ка- кой-либо математической теории, а это значит, что: такая формула дока- зуема во всех таких теориях). Содержательно это напоминает понятие об- щезначимости, но формально связь N-выводимости и общезначимости пока не установлена. Для ее установления введем еще одно исчисление - сек- венциальное, связанное, с одной стороны, с понятием истинности, а с другой - с исчислением натурального вывода. Секвенция - это конструк- ция A1,...,An -> B1,...,Bm (n,m>=0, Ai, Bj - формулы), содержательно понимаемая как "из A1,...,An следует хотя бы одно из утверждений B1,...,Bm". Списки формул A1,...,An и B1,...,Bm считаются неупорядо- ченными (т.е. A,B->C,D означает то же самое, что и B,A->D,C). Формула A выводима в секвенциальном исчислении (|-G A), если можно по правилам G-вывода построить вывод из G-аксиом секвенции ->A. Правила G-вывода таковы, что поиск вывода в этом исчислении можно осуществлять конт- рприменениями (применениями снизу вверх) правил вывода. Такой поиск вывода можно, в частности, рассматривать как попытку построения конт- рпримера для формулы A (анализируем структуру формулы A, и либо нахо- дим контрпример, либо убеждаемся, что его невозможно построить; пос- леднее наблюдается, когда все ветви вывода заканчиваются аксиомами, т.е. формула A является G-выводимой). Пусть F1 и F2 - формулы, а L и R - списки формул. Аксиома СЕКВЕНЦИАЛЬНОГО ВЫВОДА: F1,L -> R,F1. Правила СЕКВЕНЦИАЛЬНОГО ВЫВОДА. Конъюнкция: F1,F2,L->R L->R,F1 L->R,F2 (&<-) ---------- (->&) ----------------- F1&F2,L->R L->R,F1&F2 Дизъюнкция: F1,L->R F2,L->R L->R,F1,F2 (V<-) ----------------- (->V) ---------- F1VF2,L->R L->R,F1VF2 Импликация: L->R,F1 F2,L->R F1,L->R,F2 (><-) ----------------- (->>) ---------- F1>F2,L->R L->R,F1>F2 Отрицание: L->R,F1 F1,L->R (ї<-) -------- (->ї) -------- їF1,L->R L->R,їF1 Кванторы: A.vF1,(Svt)F1,L->R L->R,(Svw)F1 (A<-) ------------------ (->A) ------------ A.vF1,L->R L->R,A.vF1 (Svw)F1,L->R L->R,(Svt)F1,E.vF1 (E<-) ------------ (->E) ------------------ E.vF1,L->R L->R,E.vF1 Обозначения: w - константа, не встречающаяся в заключениях правил ->A и E<-; t - терм, свободный для v в F1; (Правила ->A и E<- называются положительными, a A<- и ->E - отрица- тельными кванторными правилами.) ---------------------------------------------------------------------------- Если рассматривать поиск вывода формулы как метод установления ее общезначимости, то возникает вопрос о корректности (правильности) это- го метода: верно ли, что если вывод построен (т.е. на вопрос "общезна- чима ли формула?" метод дает ответ "да"), то формула действительно об- щезначима? Поэтому логическое исчисление называется корректным, если в нем выводимы только общезначимые формулы (выводимость влечет общезна- чимость). Т3. Исчисление G корректно (|-G A => |=A). Д.: по определению, секвенция A1,...,An->B1,...,Bm общезначима, если общезначима соответс- твующая ей формула A1&...&An>B1V...VBm; аксиома общезначима; примене- ния (сверху вниз) правил вывода сохраняют общезначимость (для каждого правила можно показать, что если его заключение имеет контрпример, то хотя бы одна из посылок имеет конрпример). Метод установления общезначимости можно считать полным, если он дает ответ "формула общезначима" про каждую общезначимую формулу. Поэ- тому исчисление называется полным, если в нем выводимы все общезначи- мые формулы (общезначимость влечет выводимость). В исчислении G следующим образом описывается систематический ме- тод поиска вывода, позволяющий построить (может быть, бесконечное) де- рево, нагруженное секвенциями, которое либо является выводом, либо позволяет описать контрпример: 0) исходный фрагмент вывода есть дере- во, состоящее из единственной вершины, которой приписана выводимая секвенция (эта вершина - одновременно и корневая, и висячая); 1) если в построенном фрагменте вывода нет никаких пометок на формулах, то от- метим все неатомарные формулы, расположенные в висячих вершинах дерева (если таких формул нет - построение закончено); 2) если в дереве есть хотя бы одна помеченная формула, то применим (снизу вверх) подходящее правило вывода к самой левой из таких формул; если рассматриваемая по- меченная формула есть формула с квантором Qx A, к которой применимо отрицательное кванторное правило (требующее замены в формуле A пере- менной x на некоторый терм), то сопоставим формуле A множество W всех таких термов без переменных, какие присутствуют (в качестве аргументов предикатов или подтермов других термов) в ветви дерева от корня до рассматриваемой висячей вершины, но нигде ниже не подставлялись в фор- мулу A на место переменной x; если в данной ветви вообще нет термов без переменных, то в W включается одна произвольная константа; после построения W упомянутое кванторное правило применяется до тех пор, по- ка все термы из W не будут подставлены в A на место x; 3) после всех построений возникает новая висячая вершина; в соответствующей ей сек- венции пометка с рассмотренной формулы снимается, а пометки на форму- лах, не изменяемых описанными применениями правил, сохраняются; затем построение продолжается в соответствии с 1) или 2). Т4. Исчисление G полно (Если А - замкнутая формула, то |= A => |-G A). Д. Если в систематически построенном дереве вывода секвенции ->A все ветви заканчиваются аксиомами, получен вывод. Иначе есть (ко- нечная или бесконечная) ветвь, не заканчивающаяся аксиомой, и по ней можно построить (конечный или бесконечный) контрпример к формуле A. В некоторых случаях описываемый в теореме метод построения конт- рпримера дает бесконечный контрпример к формуле A, но другим способом можно построить конечный контрпример к этой же формуле. Тем не менее, существуют формулы, с одной стороны, не являющиеся общезначимыми, а с другой стороны, истинные во всех конечных интерпретациях (не имеющие конечных контрпримеров). Пусть F1 = їR(x,x); F2 = R(x,y)&R(y,z)>R(x,z); F = A.F1 & A.F2 > A.xE.y R(x,y). У формулы F су- ществует бесконечная модель (натуральный ряд с отношением строгого по- рядка), но все конечные интерпретации являются контрпримерами. Поэтому у формулы їF нет ни одного конечного контрпримера, но есть бесконеч- ный (т.е. формула не общезначима). $4. Полнота и корректность исчисления натурального вывода. Т5. Исчисление N корректно (|-N A => |=A). Д.: добавляем к G-ис- числению три правила вывода и доказываем, что их применения (сверху вниз) сохраняют общезначимость. L->R,F1 F1,L->R L->R L->R (сечение) ----------------- (утончение) ------- ------- L->R L->R,F1 F1,L->R Каждую формулу A в N-выводе заменяем на секвенцию B1,...,Bn->A, где B1,...Bn - все гипотезы, от которых A зависит; все формулы Б "сти- раем". Показываем, что в полученном "выводе" каждое применение "прави- ла" можно заменить на совокупность применений секвенциальных правил (с учетом дополнительных). Из корректности G-исчисления следует коррект- ность N-исчисления. Т6. Исчисление N полно (|= A => |-N A). Д. Модифицируем исчисле- ние G: все секвенции вида A1,...,An->B1,...,Bm превратим в A1,...,An,їB1,...,їBm->Б и соответствующим образом изменим правила вы- вода. После добавления правил Б,L->Б їA-> ----------- и ----- F1,їF1,L->Б ->A получим исчисление GM с единственной аксиомой Б,L->Б, такое что каждо- му G-выводу секвенции ->A соответствует GM-вывод этой же секвенции. Если формула общезначима, то по Т4 существует ее G-вывод. Сопоставим "готовому" GM-выводу строящую его последовательность применений правил поиска вывода в этом исчислении (они соответствуют контрприменениям GM-правил), а каждому такому правилу - последовательность применений правил поиска N-вывода. Т.к. в исходном GM-выводе все ветви заканчива- ются аксиомами, при построении этого вывода по правилам поиска вывода каждый подвывод закончится ситуацией Б |- Б. Поэтому и поиск вывода в N-исчислении завершится построением вывода. Ключевые слова к $$2-4: исчисление натурального вывода = нату- ральное исчисление = исчисление N; исчисление секвенций = секвенциаль- ное исчисление = генценовское исчисление = исчисление G; вывод=доказа- тельство; гипотеза, исключение гипотез; аксиома; правило вывода; пра- вило поиска вывода; корректность/полнота исчисления. $5. Эквивалентные преобразования формул. Отношение является отношением эквивалентности, если оно рефлек- сивно, симметрично и транзитивно. Рассмотрим 3 отношения эквивалент- ности логических формул: 1) |= (A>B) & (B>A) (собственно эквивалент- ность), 2) |=A <=> |=B (одновременная общезначимость), 3) A |= Б <=> B |= Б (одновременная невыполнимость). Формула A называется невыполнимой (противоречивой), если A|=Б. Т7 связывает эквивалентность 1 с эквивалентностями 2 и 3. Т7. Если формулы A и B собственно эквивалентны, то они одновре- менно общезначимы и одновременно невыполнимы. Д. следует из определе- ний. Замечание. Обратное не верно. Т8-11 относятся к собственно эквивалентности (эквивалентности в смысле 1). Т8. Следующие пары формул эквивалентны в смысле 1): 1) A>B и їAVB; 2) їїA и A; 3) AoB и BoA; 4) Ao(BoC) и (AoB)oC; 5) Ao(B*C) и (AoB)*(AoC); 6) ї(AoB) и їA*їB; 7) QxA и A (если A не содержит x сво- бодно); 8) QxA(x) и QyA(y); 9) їQxA и GxїA; 10) Qx(AoB) и (QxA)oB (ес- ли B не содержит x свободно); 11) A.x(B&C) и (A.xB & A.xC); 12) E.x(BvC) и (E.xB v E.xC). Обозначения: если o = &, то * = V, и наобо- рот; если Q=A., то G=E., и наоборот. Д.: построение G-выводов. Т9 (о замене эквивалентных подформул). Если формулы A и B эквива- лентны в смысле 1, и формула CB получается из CA заменой подформулы A на подформулу B, то формулы CA и CB эквивалентны в этом же смысле. Д.: индукция по глубине расположения подформулы A в формуле CA; построение G-выводов. Формула находится в предваренной нормальной форме (пнф), если имеет вид Q1x1...Qnxn B, где B - формула без кванторов (при этом выра- жение Q1x1...Qnxn называется кванторной приставкой). Т10. Любую формулу можно привести к пнф (Для любой формулы A су- ществует формула B в пнф, эквивалентная ей в смысле 1). Д. следует из Т8-9. Формула находится в конъюнктивной нормальной форме (кнф), если имеет вид A1&...&An (n>=1), где Ai - дизъюнкт, т.е. B1V...VBm (m>=1), где Bj - литера, т.е. C или їС, где С - атомарная формула. Т11. Любую формулу без кванторов можно привести к кнф. (Для любой формулы без кванторов A существует формула B в кнф, эквивалентная A в смысле 1). Д. следует из Т8-9. Т12-13 относятся к одновременной общезначимости и одновременной невыполнимости (эквивалентностям в смыслах 2 и 3). Т12. При замыкании формулы кванторами общности сохраняется общез- начимость и невыполнимость (|=F <=> |=A.F; F|=Б <=> A.F|=Б). Д. следу- ет из Т2. Пусть A=Q1x1...Qnxn B - формула в пнф (n>=0). Тогда формула С на- зывается скулемовской нормальной формой (снф) формулы A, если она по- лучена из A следующими преобразованиями: если Qi - квантор существова- ния, а Qj1,...,Qjm (m>=0) - все кванторы общности, предшествующие Qi в последовательности Q1,...,Qn, то Qixi удаляется из кванторной пристав- ки, а в формуле B каждое вхождение переменной xi заменяется на терм f(xj1,...,xjm), где f - новый m-местный функциональный символ; и т.д. для всех кванторов существования (в произвольном порядке). Т13. Если A - формула в пнф, а B - соответствующая ей формула в снф, то формулы A и B одновременно невыполнимы. Д.: показывается, что формулы A и B одновременно имеют модель: это следует из соответствия между семантикой квантора существования, которому предшествуют кванто- ры общности по переменным xj1,...,xjm и всюду определенной функции f(xj1,...,xjm). Ключевые слова к $5: эквивалентность (рефлекcивность, симметрич- ность, транзитивность); собственно эквивалентность; одновременная об- щезначимость; противоречивость=невыполнимость; одновременная невыпол- нимость; конъюнктивная/предваренная/скулемовская нормальные формы; $6. Метод резолюций (R-метод). Метод резолюций - это машинно-ориентированный метод установления общезначимости формул: составляющие его преобразования просты и не требуют "творчества", но зато лишены сколько-нибудь ясного содержа- тельного смысла (в противоположность натуральному выводу, моделирующе- му содержательное доказательство: см. таблицу). і Методы доказательства і N і G і R і Г———————————————————————Е————Е————Е————ґ і Содержательный смысл і ++ і +- і -- і Г———————————————————————Е————Е————Е————ґ і Простота действий і -- і +- і ++ і Метод резолюций можно рассматривать как доказательство общезначи- мости "от противного": отрицание рассматриваемой (замкнутой) формулы приводится к противоречию. Т14. Замкнутая формула общезначима тогда и только тогда, когда ее отрицание невыполнимо. Д.: следует из определений. Замечание. Для незамкнутых формул Т14 не верна. Метод резолюций существенно опирается на эквивалентные преобразо- вания: формула A, общезначимость которой следует установить, замыкает- ся кванторами общности; отрицание полученной формулы приводится снача- ла к предваренной нормальной форме, а затем к скулемовской нормальной форме, в то время как бескванторная часть формулы приводится к конъюн- ктивной нормальной форме. Полученная конъюнкция дизъюнктов переписыва- ется в виде множества этих дизъюнктов. К этому множеству добавляются новые дизъюнкты, получаемые по R-правилам (правилам метода резолюций) из уже существующих. Вывод заканчивается, когда удается получить "пус- той" дизъюнкт (состоящий из 0 литер и эквивалентный Б). В таком случае формула A называется R-выводимой (|-R A). Для упрощения вида R-правил используется представление дизъюнкта в виде множества литер, например, A(x)VїB(a)VїB(a) ---> {A(x),їB(a)}. Подстановкой называется множество б = {x1:=t1,...,xn:=tn}; Aб означает результат одновременной замены в выражении A переменных x1,...,xn на термы t1,...,tn (A может быть термом, бескванторной формулой, множеством литер). Подстановка б, та- кая что Aб = Bб, называется унификатором выражений A и B, а процесс построения такой подстановки - унификацией. Пусть С1, С2 - множества литер. R-правила: R1. С1/C1б; R2. C1; C2 / (C1-{L1})U(C2-{L2}), если L1 и L2 - контрарная пара литер (одна литера - атом, а другая - отрицание этого атома); дизъ- юнкт, получаемый в результате применения этого правила, называется ре- зольвентой дизъюнктов С1 и С2. Замечание. Применение правила R1 позволяет выполнить: 1) перео- бозначение переменных в дизъюнкте; 2) склейку нескольких литер дизъюн- кта в одну, например, A(x)VA(a){x:=a} / A(a); 3) унификацию атомов из разных дизъюнктов с целью получения контрарной пары литер L1 и L2 для последующего применения правила R2. T15. Метод резолюций корректен (|-R A => |=A). Д. По Т8-14 форму- ла A общезначима <=> соответствующее множество дизъюнктов В1 невыпол- нимо; дальше применениями R-правил выполняется преобразование В1->B2->...->Bm, причем Bm содержит Б, так что отношение Bm|=Б выпол- нено. Поскольку R-правила сохраняют невыполнимость, Вi|=Б <=> Bi+1|=Б. Т16. Метод резолюций полон (|=A => |-R A). Д. Пусть A - замкнутая формула и |=A. Тогда їA эквивалентна некоторой формуле B в снф и кнф, причем B|=Б, |=їB и существует G-вывод формулы їB. "Разбирая" этот вы- вод (удаляя из него контрарные пары), построим вывод пустого дизъюнкта по R-правилам. Ключевые слова к $6: метод резолюций=R-метод; унификатор=унифици- рующая подстановка, унификация; множество дизъюнктов, множество литер, контрарная пара. $7. Эрбрановские интерпретации. Логику высказываний (ЛВ) можно рассматривать как частный случай логики предикатов (ЛП): в ЛВ все предикаты 0-местные и, следовательно, могут принимать только одно истинностное значение (истина/ложь) в каж- дой данной интерпретации. Поэтому с точки зрения ЛВ неразличимы мно- жества, на которых строятся интерпретации, и можно (условно) считать, что всегда рассматривается одно и то же множество, а разные интерпре- тации отличаются друг от друга истинностными значениями 0-местных пре- дикатов. Следовательно, множество всех интерпретаций формулы ЛВ конеч- но и ее общезначимость может быть установлена полным перебором (пост- роением истинностной таблицы), т.е. безо всякого логического вывода. В ЛП понятие общезначимости учитывает различные (в том числе бесконеч- ные) множества, и на них по-разному интерпретируются не только преди- каты, но и функции. Но использование эрбрановских интерпретаций (ЭИ) позволяет упростить эту ситуацию (см. таблицу). Интерпретация: і множество і функции і предикаты і ———————————————Е—————————————Е—————————————Е————————————ґ ЛВ і одно і нет і интерпрет. і і (условное) і і по-разному і ———————————————Е—————————————Е—————————————Е————————————ґ ЛП і много і интерпрет. і интерпрет. і і і по-разному і по-разному і ———————————————Е—————————————Е—————————————Е————————————ґ ЛП і одно і интерпрет. і интерпрет. і с учетом ЭИ і і одинаково і по-разному і ———————————————Б—————————————Б—————————————Б————————————Щ ЭИ - это интерпретация формулы на множестве, называемом ее эрбра- новским универсумом, и именно, множестве всех термов, которые можно построить из констант и функций данной формулы (если нет констант, фиксируется какая-либо произвольная); такие термы называются основны- ми. Функции интерпретируются так, чтобы значением каждого терма был он сам. Предикаты интерпретируются как истинностные функции на множестве термов. Основное свойство эрбрановской интерпретации: в ней истинност- ное значение любой атомарной формулы без переменных P(t1,...,tn) сов- падает с P^('t1',...,'tn'), где 't1',...,'tn' - элементы эрбрановского универсума. Эрбрановский базис формулы - это множество всех атомарных формул, которые можно построить из предикатов этой формулы и термов ее эрбрановского универсума; такие атомы называются основными. Каждую ЭИ можно задать как подмножество эрбрановского базиса (атомарная формула истинна в данной ЭИ <=> принадлежит подмножеству). Основной пример дизъюнкта С - это дизъюнкт Сб, где б - подстановка термов из эрбра- новского универсума на места всех переменных С. Т17 (теорема Эрбрана). Множество дизъюнктов S невыполнимо <=> не- выполнимо некоторое конечное множество S' основных примеров этих дизъ- юнктов. Д. (=>): Пусть D=ї(С1&...&Cn), где C1,...,Cn - замыкания кван- торами общности всех дизъюнктов из S. S невыполнимо => |=D. Построим G-вывод D при помощи систематического метода поиска вывода. В этом вы- воде при снятии кванторов общности отрицательными кванторными правила- ми будут подставляться только термы из эрбрановского универсума (т.к. по определения систематического метода подставляются только термы без переменных, и не применяются положительные кванторные правила, порож- дающие новые константы). Этот вывод можно преобразовать в такой, в ко- тором сначала применяются только правила снятия кванторов, а затем все остальные. Т.к. все ветви заканчиваются аксиомами вида A,L->L,B, где L основной атом, то в них ниже есть основные примеры дизъюнктов, содер- жащих L и їL. Удаляя из вывода участок, на котором снимаются кванторы, получим вывод секвенции, содержащей справа пустой набор формул, а сле- ва только основные примеры некоторых дизъюнктов из С1,...,Сn. (=>): Если дан вывод такой секвенции, то расположив ниже последовательность правил А-> с подстановками, порождающими именно эти основные примеры дизъюнктов, получим вывод ->D. Т18. Множество дизъюнктов S невыполнимо <=> S ложно во всех эрб- рановских интерпретациях. Д. (=>): очевидно. (<=): от противного. Пусть S имеет модель I. Если в S нет констант, и при построении эрбра- новского универсума добавляется константа w, построим I', добавив к I какую-либо интерпретацию для w. Иначе положим I'=I. В I' все основные атомы (атомы из эрбрановского базиса S) принимают определенное значе- ние истина/ложь, а все основные примеры дизъюнктов из S истинны (пос- кольку дизъюнкты с переменными истинны в I при любых значениях пере- менных). Построим эрбрановскую интерпретацию Ih = { P('t1',...,'tn') | P(t1,...,tn) - основной атом и I' |= P(t1,...,tn) }. В этой ЭИ каждый основной пример дизъюнкта имеет то же истинностное значение, что и в I', т.е. является истинным, а следовательно и каждый дизъюнкт с пере- менными является истинным при любых значениях переменных из эрбрановс- кого универсума. Следовательно Ih является эрбрановской моделью S. Ключевые слова к $7: эрбрановские универсум /базис /интерпрета- ция; основной терм/атом/пример дизъюнкта. Замечание. Часть I построена по следующему плану: Ъ———————ї ЙНННННННННННН»————————————>іЯзык ЛПі ЙНННННННННННН» є Содержа- є Ъ—————————Е———————Е——————————ї є Логическое є є тельная є——>і Исч.N і Исч.G і Метод R Г——>є програм- є є математика є А—————————Е———————Е——————————Щ є мирование є ИННННННННННННј і ЭИ Г—————————————>ИННННННННННННј А———————Щ Часть II. Логическое программирование. $1. Дедуктивный поиск ответов на вопросы. Концепция логического программирования: описываем аксиомами усло- вия задачи и ставим вопросы о следствиях этих аксиом, а ответы получа- ем автоматически, не строя алгоритма поиска. Возможно ли это? Под де- дуктивным поиском ответа на вопрос понимается сведение этого поиска к доказательству какой-либо теоремы в аксиоматической теории. Задачи "на доказательство" в аксиоматических теориях могут быть сформулированы в виде A |= B, где A - совокупность аксиом, а B - тео- рема, и, следовательно, сводятся к доказательству общезначимости фор- мулы A>B. Задачи "на построение" можно записать аналогично: найти терм t, такой что A |= B(t), но такая формулировка, вообще говоря, не поз- воляет свести их к доказательству какой-либо формулы (теорема о дедук- ции не применима, т.к. здесь t - символ, обозначающий неизвестный терм, и B(t) не является формулой логики предикатов). Поскольку B(t)|=E.x B(x), то решение задачи "найти объект" всегда влечет доказа- тельство существования объекта. В некоторых случаях возможен обратный порядок действий: построение доказательства формулы A>E.xB(x), и "изв- лечение" из него информации о терме t, для которого A|=B(t). Такие до- казательства называются конструктивными. Но в классической логике (рассматриваемой здесь) не все доказательства конструктивны. Тем не менее, для некоторых классов задач дедуктивный поиск ответов возможен. $2. Хорновские дизъюнкты. Дизъюнкт называется хорновским, если содержит ровно одну положи- тельную литеру и несколько (возможно, 0) отрицательных: їA1 V...V їAn V A0 (дизъюнктивная форма) или A1 &...& An > A0 (импликативная форма). Пусть P - множество хорновских дизъюнктов. Обозначим как Hp и Bp его эрбрановские универсум и базис, соответственно. Интерпретации I множества P будем задавать в виде подмножеств Bp. Т19. Любое множество хорновских дизъюнктов имеет модель. Д. Bp множества P является его моделью. Следствие. Множество хорновских дизъюнктов непротиворечиво. Т20 (о пересечении эрбрановских моделей). Пересечение каких-либо эрбрановских моделей множества хорновских дизъюнктов является эрбра- новской моделью этого множества. Д.: если пересечение - не модель, то среди пересекающихся интерпретаций можно указать интерпретацию, не яв- ляющуюся моделью. Замечание. Для произвольных дизъюнктов теорема не верна. Обозначим как Mp пересечение всех эрбрановских моделей P. Пос- кольку Мр является подмножеством любой эрбрановской модели Р, назовем Мр наименьшей эрбрановской моделью Р. Следствие. Любая эрбрановская модель множества хорновских дизъюн- ктов является подмножеством Bp и содержит Mp в качестве подмножества. Т21 (об устройстве Мр). Пусть P* - множество всех основных приме- ров P. Тогда атом A принадлежит Мр <=> в P* есть дизъюнкт A1&...&An>A и атомы A1,...,An принадлежат P*. Д. (=>): если атом B принадлежит Мр, но не обладает указанным свойством, Mp-{B} тоже эрбрановская модель, что противоречит условию: Mp - наименьшая эрбрановская модель. Следствие. Mp можно построить так: 0) построим P*; 1) возьмем все атомы из P*; 2) добавим все такие A, что в Р* есть A1&...&An>A и A1,...,An включены в Мр на одном из предыдущих шагов; 3) и т.д., пока добавление возможно (может быть, до бесконечности). $3. Декларативная семантика Пролога. Чистый Пролог: пусть A,A1,...,An - атомарные формулы. Тогда <программа>::=<программные утверждения><запрос> <программное утверждение>::=<правило>|<факт> <правило>::= A:-A1,...,An. <———ї A1,...,An - тело правила <факт>::= A. <——————————Щ A - голова прогр.утверждения <запрос>::= ?A1,...,An. Сопоставим всем программным утверждениям хорновские дизъюнкты: A:-A1,...,An. --> A1&...&An>A; A. --> A, а запросу - формулу A1&...&An. Пусть P - полученное множество хорновских дизъюнктов, а Q - формула, соответствующая запросу. Пару будем также называть программой (или формульным представлением программы). Декларативная семантика программы - это характеризация (описание на некотором языке) множества ответов программы без указания алгоритма их построения (ответ на вопрос: ЧТО вычисляет программа?). Декларатив- ная семантика Пролога формулируется в терминах логического следования, а именно: ответом программы называется подстановка б={x1:=t1,...,xn:=tn} термов на места всех переменных Q, удовлетворяю- щая условию: P|=Qб. Если подстановка б является пустым множеством (т.е. Q не содержит переменных и P|=Q), то ответ б понимается как "да". Вопрос: если даны P и Q, то что можно сказать о б? Т22 (о главном свойстве наименьшей эрбрановской модели). Пусть Р - множество хорновских дизъюнктов и атом A является элементом эрбра- новского базиса Bp. Тогда A принадлежит Mp <=> P|=A. Д. Множество дизъюнктов PU{їA} невыполнимо <=> оно ложно во всех эрбрановских ин- терпретациях <=> формула їA ложна во всех эрбрановских моделях P <=> А принадлежит Mp. Замечание. T22 утверждает, что 1) Мр - это множество основных атомов, являющихся теоремами по отношению к системе аксиом P; 2) Mp - это множество запросов Q, являющихся основными атомами, на которые программа отвечает "да". Пусть Hpq - множество основных термов, построенных с использова- нием всех функциональных символов из ; Bpq - множество всех ос- новных атомов, построенных из предикатов, встречающихся в P и термов, встречающихся в Hpq; Mpq - множество основных атомов, образованное по правилам построения наименьшей эрбрановской модели, но с учетом Hpq вместо Hp (т.е. Р* - множество основных примеров дизъюнктов, получен- ных подстановками термов из Hpq в P). Тогда Mpq - эрбрановская интерп- ретация для Q. Т23 (о декларативной семантике). Пусть - программа. Если б - некоторая подстановка термов из Hpq на места всех переменных Q, то б является ответом программы <=> Mpq |= Qб. Д. К множеству Р добавим "фиктивный" дизъюнкт A(t1,...,tn)>A(t1,...,tn), где термы t1,...,tn содержат все функциональные символы и константы, входящие в Q, но не входящие в P, а А - предикатный символ, не встречающийся в . По- лученное множество дизъюнктов назовем P'. Пусть б - подстановка из ус- ловия теоремы. Тогда P|=Qб <=> P'|=Qб <=> Mp'|=Qб <=> Mpq |= Qб (с учетом тождественной истинности добавленного дизъюнкта, Т22 и правил построения наименьшей эрбрановской модели). Замечание. Т23 характеризует не все ответы программы. $4. SLD-резолюция. Композиция подстановок: операция, сопоставляющая двум последова- тельным подстановкам - одновременную. Т24 (о композициях подстановок): тождественная (пустая) подста- новка является левой и правой единицей; (Aб1)б2 = A(б1б2); композиция ассоциативна. Д. ... Пусть - программа, Q±&...&Bk&...&Bm, Cб&...&An>A - эле- мент P и Aб = Bkб. Тогда SLD-резольвентой с подстановкой б называется конъюнкция (возможно, "пустая": из 0 элементов) Q'б, где Q' получается из Q заменой Bk на A1&...&An. SLD-последовательностью для программы Q0 называется последовательность троек (Qi,Ci,бi), ії такая что Ci - элемент P, Qi - SLD-резольвента Q1———C1, б1 Qi-1 и Ci c подстановкой бi, Q0=Q (каждая из ії формул Qi называется текущим запросом). Q2———C2, б2 Если Qn - пустая конъюнкция, то SLD-после- ... довательность называется SLD-выводом программы ії , строящим подстановку б'=б1...бn и вычис- Qn———Cn, бn ляющим подстановку б на места всех переменных Q, являющуюся подмножеством б'. T25 (о корректности SLD-резолюции). Если SLD-вывод для программы вычисляет б, то б - ответ этой программы. Д.: индукция по длине вывода. При построении SLD-последовательности может быть фиксировано (для всех текущих запросов одновременно) некоторое правило выбора Bk из Qi±&...&Bk&...&Bm. А именно, пусть R(m) - функция, сопоставляющая каждому натуральному числу m натуральное число k: 1<=k<=m. Тогда SLD-последовательность с правилом выбора R есть такая SLD-последова- тельность, в которой на каждом шаге выбирается Bk, k=R(m). T26 (о полноте SLD-резолюции с правилом выбора). Если б - ответ программы , то существует SLD-вывод этой программы с фиксирован- ным правилом выбора подцели, вычисляющий подстановку б. Д.: 2 случая: 1) б - подстановка термов из Hpq на места всех переменных Q - Д. сле- дует из Т о декларативной семантике; 2) Qб содержит переменные - сво- дится к 1). В случае 1 строится дерево, соответствующее Mpq. Разбирая это дерево (удаляя контрарные пары), получим SLD-вывод для программы . Следствие. SLD-резолюция без правила выбора также полна. Замечание. Можно без потери общности считать фиксированным прави- ло выбора R(m)=1. Понятия: наиболее общего унификатора (НОУ); множества рассогласо- ваний; алгоритма унификации (АУ) (см. Чень, Ли: "Мат. логика и автома- тическое доказательство теорем"). Т27 (об АУ). Если W - унифицируемое множество выражений, то АУ выдает сообщение "б - НОУ" и б действительно есть НОУ. Д.: см. Чень,Ли. SLD-последовательность с НОУ есть такая SLD-последовательность, в которой на каждом шаге в качестве унифицирующей подстановки выбирается НОУ. Т28 (о полноте SLD-резолюции с НОУ). Если SLD-вывод для программы вычисляет подстановку б1, то для этой программы существует SLD-вывод с НОУ такой же длины, вычисляющий подстановку б2 = б1 б. Д.: индукцией по длине вывода. В построенном SLD-выводе все "избыточные" подстановки "сдвигаются" к концу, образуя б. Замечание. SLD-выводы с НОУ строят не все ответы программы. $5. Процедурная семантика Пролога. Процедурная (императивная) семантика программы - это описание процесса построения ее ответов (ответ на вопрос: КАК вычисляет прог- рамма?). Процедурная семантика Пролога формулируется в терминах поиска SLD-выводов. SLD-дерево (дерево вычислений) - это растущее сверху вниз дерево, каждая ветвь которого - SLD-последовательность с правилом вы- бора R(m)=1 и с НОУ, причем непосредственно ниже каждой тройки (Q,C,б), где Q±&...&Bn, располагаются все тройки, содержащие прог- раммные утверждения C1,...,Cl, головы которых унифицируемы с B1. Замечания. 1) SLD-дерево содержит все возможные SLD-последова- тельности; 2) ветви SLD-дерева могут быть выводами, тупиковыми (не имеющими продолжений) или бесконечными; 3) каждый SLD-вывод (и только он) вычисляет некоторый ответ программы; 4) престановка программных утверждений не влияет на конечность/бесконечность дерева и на множест- во вычисляемых ответов; 5) перестановка атомов в теле программного ут- верждения влияет на конечность/бесконечность дерева, но не влияет на множество ответов. Стандартная стратегия обхода (или построения) SLD-дерева: подхо- дящие С1,...,Сl упорядочиваются (слева направо) в соответствии с их порядком (сверху вниз) в программе; обход дерева осуществляется "вглубь" (спуск по крайней левой еще не пройденной ветви до конца, за- тем возврат на ближайшую снизу развилку, и т.д.). Замечания. 1) Стандартная стратегия корректна, но не полна: попав на бесконечную ветвь, никогда не дойдем до более правых ветвей. Поэто- му если SLD-дерево бесконечно, то вычисление продолжается до бесконеч- ности, и при этом могут перечисляться как все, так и не все ответы. 2) Пусть Q±,...,Bn - текущий запрос. Тогда каждый атом Вi - его под- цель. Подцель называется успешной, если существует SLD-вывод программы , и неуспешной в противном случае. Если подцель Bi успешна, то следующей рассматривается подцель Bi+1, а если неуспешна, происходит поиск другого вывода для подцели Bi-1. Операторы Пролога fail, ! (cut) и not не имеют удовлетворительной декларативной семантики в терминах классической логики, но имеют про- цедурную семантику в терминах построения SLD-дерева. А именно: fail есть всегда неуспешная подцель. Если в теле некоторого программного утверждения С содержится опе- ратор !(сut), и голова этого программного утверждения унифицируется с атомом текущего запроса, приписанного вершине R1, то ниже этой вершины может встретиться вершина R2 с текущим запросом !,.... В таком случае ! - успешная подцель, но при возврате переход из R2 осуществляется сразу в вершину R0, непосредственно предшествующую R1 (если R0 нет, вычисление заканчивается). Подцель not(В) успешна, если неуспешна В, и наоборот. Поэтому оператор not в Прологе носит название "отрицание как неудача". Декла- ративная семантика этого оператора соответствует принятию "гипотезы замкнутости мира". А именно, "мир", описываемый программными утвержде- ниями P, считается "замкнутым" в том смысле, что те суждения, которые не являются в нем истинными, полагаются ложными. Пусть для некоторого атома A верно: P|=A. Тогда не верно, что Р|=їА. Но если для атома B не верно, что Р|=В, то Р|=їВ также не верно (последнее отношение равно- сильно отношению Р,В|=Б, которое не выполнено в силу непротиворечивос- ти любого множества хорновских дизъюнктов). Поэтому для построения ма- тематической модели гипотезы замкнутости мира вводится новое (отличное от классического ї) отрицание ~: P|=~B <=> не верно, что P|=B. Отрица- ние как неудача соответствует отрицанию ~ в полном SLD-дереве, но в случае применения стандартной стратегии построения этого дерева отно- шение P|=B может оказаться не установленным (при попадании на беско- нечную ветвь). Поэтому процедурная семантика not корректна по отноше- нию к декларативной, но не полна. $6. Дедуктивный поиск ответов на вопросы. Окончание. T29 (о конструктивности классической логики по отношению к прог- раммам). Если - программа, и P|=E.Q (где E.Q - замыкание формулы Q кванторами существования), то существует подстановка б, такая что P|=Qб. Д. аналогично доказательству Т22 и Т23. Можно ли найти эту подстановку методом резолюций? Преобразуем P|=E.Q в |=A.P>E.Q, а затем в A.P & A.їQ |=Б. Если Q±&...&Bm, то їQ эквивалентно їB1V...VїBm. Приведение к скулемовской нормальной форме не изменяет формулу A.P & A.їQ. Т.к. P|=Qб, существу- ет SLD-вывод, вычисляющий б. Если представить хорновские дизъюнкты из P в дизъюнктивной форме, а запрос Q±&...&Bm - в виде Q'=їB1V...VїBm, то SLD-вывод программы превратится в вывод методом резолюций для множества дизъюнктов PU{Q'}, так что SLD-резолюцию можно рассматривать как стратегия метода резолюций, полную на множестве программ. Следствия: 1) программы - это как раз те задачи, для которых воз- можен дедуктивный поиск ответов на вопросы (в частности - методом ре- золюций); 2) программа имеет хотя бы один ответ <=> формула A.P>E.Q является общезначимой. Ключевые слова к $$1-6: дедуктивный поиск ответов на вопросы, конструктивность, хорновский дизъюнкт, наименьшая эрбрановская модель, SLD-резолюция, SLD-последовательность/вывод/дерево, правило выбора подцели, наиболее общий унификатор, алгоритм унификации, декларатив- ная/процедурная семантика, стандартная стратегия вычисления, гипотеза замкнутости мира. $7. Алгоритмическая полнота чистого Пролога. Неформальное понятие алгоритма (решает массовую проблему; состоит из элементарных шагов: однозначно ясно, как его выполнить, что являет- ся результатом и какой шаг следующий). Функция называется интуитивно вычислимой, если ее вычисляет некоторый алгоритм. Функция называется вычислимой, если ее вычисляет некоторая машина Тьюринга. Тезис Черча: множество интуитивно вычислимых функций совпадает с множеством вычислимых. Алгоритмический язык (в частности, язык программирования) называ- ется алгоритмически полным, если для любой вычислимой функции сущест- вует программа на этом языке, ее вычисляющая. Пролог-программа вычисляет (не всюду определенную) функцию f(x) <=> для любых a и b, таких что f(a)=b, SLD-дерево конечно и содержит единственный вывод, вычисляющий подста- новку {y:=b}, а для любого c, такого что значение f(c) не определено, SLD-дерево бесконечно и не содержит выводов. T30 (об алгоритмической полноте Пролога). Если функция f(x) (не обязательно всюду определенная) вычисляется некоторой машиной Тьюрин- га, то существует Пролог-программа, вычисляющая эту же функцию. Д.: моделирование программы машины Тьюринга Пролог-программой. $8. Проблема общезначимости в логике предикатов. (Массовая) проблема называется разрешимой, если существует всюду определенный алгоритм, ее решающий. В частности, разрешимость проблемы общезначимости формул логики предикатов означает существование алго- ритма, по любой формуле однозначно определяющего: общезначима эта фор- мула или нет. Сопоставим программе формулу A.P > E.Q . T31. Проблема общезначимости формул, соответствующих программам, не разрешима. Д.: сведение к проблеме остановки. Если всегда можно ус- тановить общезначимость формулы A.P > E.Q, то всегда можно установить, имеет ли хотя бы один ответ программа . Но это означает возмож- ность установить, закончит ли работу произвольная машину Тьюринга (т.к. ее можно смоделировать в виде Пролог-программы). Последнее про- тиворечит неразрешимости проблемы остановки. Следствие. Не существует алгоритма, по тексту Пролог-программы определяющего: 1) имеет ли она ответы; 2) заканчивает ли она работу. T32. (Теорема Черча о неразрешимости логики предикатов). Проблема общезначимости формул логики предикатов не разрешима. Д. доказательст- во следует из Т31. Ключевые слова к $$7-8: алгоритм; алгоритмическая полнота; машина Тьюринга; тезис Черча; разрешимость массовой проблемы; проблема общез- начимости.