Как вывести пустой дизъюнкт
На этом шаге мы рассмотрим доказательство общезначимости и противоречивости формул в логике предикатов первого порядка .
В отличие от логики высказываний в логике предикатов первого порядка имеется очень большое число интерпретаций формулы, поэтому общезначимость или противоречивость этой формулы невозможно доказать проверкой ее истинности при всех возможных интерпретациях.
В логике предикатов первого порядка не существует никаких алгоритмов, проверяющих общезначимость формулы, но существуют алгоритмы, которые могут ее подтвердить.
По определению общезначимой называется формула, которая истинна при всех интерпретациях. Существуют алгоритмы нахождения такой интерпретации, при которой формула ложна. Однако, если данная формула общезначима, то не существует такой интерпретации, при которой формула была бы ложна.
Поскольку формула общезначима тогда и только тогда, когда ее отрицание противоречиво, то можно установить противоречивость отрицания данной формулы. Это служит основой для большинства современных автоматических алгоритмов поиска доказательства.
Наиболее эффективно поиск доказательств общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, то есть вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво.
Суть метода резолюций состоит в следующем. Пусть S — множество дизъюнктов, которые представляют стандартную форму формулы F . Тогда F противоречива в том и только в том случае, когда противоречиво S . Если S содержит пустой дизъюнкт, то S невыполнимо. Если S не содержит пустой дизъюнкт, то проверяется, может ли пустой дизъюнкт быть получен из S .
Процедура опровержения применима, если формула находится в стандартной форме, введенной Дэвисом и Патнемом . Для преобразования формулы к стандартной форме ими были использованы следующие положения:
- в логике предикатов первого порядка формула может быть приведена к предваренной нормальной форме , когда матрица не содержит никаких кванторов, а префикс есть последовательность кванторов;
- поскольку матрица не содержит кванторов, она не может быть представлена в конъюнктивной нормальной форме;
- сохраняя противоречивость формулы, в ней можно уничтожить кванторы существования, заменив переменные, попадающие в область действия кванторов существования, константами.
Дизъюнктом называется дизъюнкция литер. Множество литер можно рассматривать как синоним дизъюнкта.
Дизъюнкт, содержащий n литер, называется n- литерным дизъюнктом .
Однолитерный дизъюнкт называется единичным дизъюнктом .
Дизъюнкт называется пустым , если он не содержит никаких литер. Пустой дизъюнкт всегда ложен, так как в нем нет литер, которые могли бы быть истинными при любых интерпретациях.
Метод резолюций для логики высказываний
Метод резолюций можно применять к любому множеству дизъюнктов с целью проверки их невыполнимости (противоречивости). Рассмотрим сначала метод резолюций для логики высказываний.
A называются контрарными , а множество A> – контрарной парой. Допустим, что в дизъюнкте C 1 существует литера L 1 , контрарная литере L 2 в дизъюнкте C 2 . Вычеркнем литеры L 1 и L 2 из дизъюнктов C 1 и C 2 соответственно и построим дизъюнкцию оставшихся дизъюнктов. Построенный дизъюнкт называется резольвентой дизъюнктов C 1 и C 2 . Резольвента двух дизъюнктов является их логическим следствием. Резольвента двух единичных дизъюнктов (если она существует) – пустой дизъюнкт. Резолютивный вывод C из множества дизъюнктов S есть такая конечная последовательность C 1 , C 2 , . C k дизъюнктов, в которой каждый C i (i=1, . k) или принадлежит S , или является резольвентой дизъюнктов, предшествующих C i и C k =C . Дизъюнкт C может быть выведен или получен из S , если существует вывод C из S . Для невыполнимого множества дизъюнктов в результате последовательного применения правила резолюций получается пустой дизъюнкт. Вывод из множества S пустого дизъюнкта называется опровержением (доказательством невыполнимости) S .Метод резолюций для логики предикатов первого порядка
Нахождение в двух дизъюнктах контрарных литер выполняется довольно просто, если дизъюнкты не содержат переменных. Дизъюнкты, содержащие переменные, необходимо унифицировать, то есть найти такую подстановку, в результате которой исходные дизъюнкты будут содержать контрарные литеры.
Рассмотрим несколько примеров.
Пусть формулы A(x) и A(b) не тождественны. В формуле A(x) встречается переменная x , а в A(b) – константа b . Чтобы отождествить A(x) и A(b) , заменим переменную x на константу b , то есть присвоим переменной x значение b . В результате получаем A(x)=A(b) .
Рассмотрим дизъюнкты: D 1 : A(x) B(x),
D 2 :
A(f(y)) C(y),
которые не содержат контрарных литер. Если в D 1 подставить f(a) вместо x , а в D 2 – значение a вместо y , то дизъюнкты преобразуются к следующему виду:
A(f(a)) контрарны, то получим резольвенту дизъюнктов D 1 и D 2 в виде:
Дизъюнкты имеют одну или несколько резольвент, так как возможны разные подстановки. Любую подстановку можно представить с помощью множества упорядоченных пар t i /x i :
где t i – терм, x i – переменная, i=1, . n .
Пара t i /x i означает, что переменная x i повсюду заменяется на терм t i . Переменная не может быть заменена на терм, содержащий ту же самую переменную, например переменную x i нельзя заменить на терм t i =f(x i ) .
Если подстановка S применяется к каждому члену некоторого множества
Обычно унификацию используют для того, чтобы показать, можно ли литеры привести в соответствие между собой. Для этого в литерах вместо переменных надо подставить термы.
Процесс сопоставления некоторого выражения с эталонным называется сопоставлением с образцом. Он играет важную роль в системах искусственного интеллекта.
Одна и та же задача с помощью формул логики предикатов первого порядка может быть записана в различной форме. Представляется целесообразным, особенно для выполнения формальных преобразований, использование стандартной формы записи выражений.
На следующем шаге мы рассмотрим семь этапов приведения формул к стандартной форме записи .
Источник
Большая Энциклопедия Нефти и Газа
Вывод — пустой дизъюнкт
Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем — пустой дизъюнкт. [1]
Таким образом мы в процессе поиска вывода пустого дизъюнкта систематически перебираем возможные подстановки и унификации. [2]
Входное ( единичное) опровержение-это входной ( единичный) вывод пустого дизъюнкта . [3]
Каждый из дизъюнктов Ri, i e l: m, является возможным центральным дизъюнктом, который может привести к выводу пустого дизъюнкта . Если при этом RI пустой дизъюнкт, то решение задачи найдено. В противном случае для каждого Ri находим все возможные боковые дизъюнкты, подходящие для резольвенции с RJ в качестве центрального дизъюнкта, и продолжаем этот процесс до тех пор, пока не будет порожден пустой дизъюнкт. [4]
Метод резолюций, получив на вход логическую программу с присоединенным к ней запросом в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта , обозначаемого символом D. Если это ему удается, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюций с помощью двух правил: правила резолюции и правила склейки, которые во время работы вызывают процедуру унификации — сопоставления. [5]
Приведенное только что доказательство может создать у читателя впечатление, что ИР не дает ничего по сравнению с теоремой Эрбрана, так как высота вывода пустого дизъюнкта в Ир — это в точности размер эрбрановской дизъюнкции. [6]
Более детальная характеризация корректности и полноты SLD-резолюции получается путем включения в рассмотрение как решений целевого утверждения ( подстановок, дающих ответ), вычисляемых посредством вывода пустого дизъюнкта П, так и правила вычислений, используемого для их нахождения. Правило вычислений — это любое фиксированное правило, однозначно определяющее, какие из вызовов, содержащихся в текущем целевом утверждении, отрезаются на каждом шаге SLD-резолюции. [7]
Какое бы правило вычислений ни применялось к программе, в Является подстановкой, дающей правильный ответ для программы, тогда и только тогда, когда она вычислима посредством вывода пустого дизъюнкта П с помощью SLD-резолюции. [8]
Если мы хотим написать машинную программу, которая будет делать за нас резолюцию и искать ответы на вопросы, то мы должны сообщить ей какие-то наводящие соображения, или эвристики, чтобы помочь в поиске вывода пустого дизъюнкта . Более подробно этот вопрос рассматривается в [19] и [86], но наиболее полезные методы таковы. [9]
Возвращаясь к примеру 1.10, в котором детектив должен доказать, что, если горничная сказала правду, то дворецкий солгал, мы видели, что дерево вывода ( см. рис. 1.2) линейно, и вывод пустого дизъюнкта был получен с помощью входной резолюции. В этом примере все дизъюнкты из S были хорновскими в отличие от примера 1.24, где дизъюнкт Р V Q — нехорновский. [10]
Литера, чье отрицание отсутствует во множестве дизъюнктов, называется чистой. Дизъюнкт, содержащий чистую литеру, естественно, не может участвовать в выводе пустого дизъюнкта и поэтому может быть удален из множества дизъюнктов. [11]
Источник
Вывод в логических моделях. Метод резолюций
Вывод в формальной логической системе является процедурой, которая из заданной группы выражений выводит отличное от заданных семантически правильное выражение. Эта процедура, представленная в определенной форме, и является правилом вывода. Если группа выражений, образующая посылку, является истинной, то должно гарантироваться, что применение правила вывода обеспечит получение истинного выражения в качестве заключения.
Наиболее часто используются два метода. Первый – метод правил вывода или метод естественного (натурального) вывода, названный так потому, что используемый тип рассуждений в исчислении предикатов приближается к обычному человеческому рассуждению. Второй – метод резолюций. В его основе лежит исчисление резольвент.
В этой статье рассматривается второй метод. Метод резолюций предложен в 1930г. в докторской диссертации Эрбрана для доказательства теорем в формальных системах первого порядка.
Метод резолюций опирается на исчисление резольвент. Существует теорема, утверждающая, что вопрос о доказуемости произвольной формулы в исчислении предикатов сводится к вопросу о доказуемости пустого списка в исчислении резольвент. Поэтому доказательство того, что список формул в исчислении резольвент пуст, эквивалентно доказательству ложности формулы в исчислении предикатов.
Идея метода резолюций заключается в том, что доказательство истинности или ложности выдвинутого предположения, например:
ведется методом от противного. Для этого в исходное множество предложений включают аксиомы формальной системы и отрицание доказываемой гипотезы:
Если в процессе доказательства возникает противоречие между отрицанием гипотезы и аксиомами, выражающееся в нахождении пустого списка (дизъюнкта), то выдвинутая гипотеза правильна.
Такое доказательство может быть получено на основании теоремы Эрбрана, гарантирующей, что существующее противоречие может быть всегда достигнуто за конечное число шагов, каковы бы ни были значения истинности, даваемые функциям, присутствующим в гипотезах и заключениях.
В методе резолюций множество предложений обычно рассматривается как составной предикат, содержащий несколько предикатов, соединенных логическими функциями и кванторами существования и общности. Так как одинаковые по смыслу предикаты могут иметь разный вид, то предложения преобразуются в клаузальную форму – разновидность конъюнктивной нормальной формы (КНФ), в которой удалены кванторы существования, всеобщности, символы импликации, равнозначности и др. Клаузальную форму называют сколемовской конъюнктивной формой.
В клаузальной форме вся исходная логическая формула представляется в виде множества предложений (клауз) 
, называемых клаузальным множеством 
:
Любое предложение , из которого образуется клаузальное множество , является совокупностью атомарных предикатов или их отрицаний, соединенных символом дизъюнкции:
Предикат или его отрицание называется дизъюнктом, литералом, атомом, атомарной формулой.
Сущность метода резолюций состоит в проверке, содержит или не содержит пустое предложение 
. Предложение является пустым, если не содержит никаких литер. Так как условием истинности является истинность всех , входящих в , то ложность какого-либо , заключающаяся в том, что множество 
, образующее , окажется пустым, указывает на ложность исходной логической формулы.
Если содержит пустое предложение , то противоречиво (невыполнимо). Если предложение не является пустым, то делается попытка вывода предложений 
пока не будет получено пустое (что всегда будет иметь место для невыполнимого ).
Для этого в двух предложениях, одно из которых состоит из одной литеры, а второе содержит произвольное число литер, находится контрарная пара литер (например 
и 
), которая вычеркивается, а из оставшихся частей формируется новое предложение (например из и 
выводится 
).
Предложение , вновь сформированное из имеющихся 
и 
, называется резольвентой и . Например:
Если при выводе предложений получены два однолитерных дизъюнкта, образующих контрарную пару, то их резольвентой будет пустой дизъюнкт. Так как наличие пустого дизъюнкта означает, что является ложным, то невыполнимость исходного утверждения, сформулированного в виде отрицания:
доказывает истинность выдвинутого предположения:
Поскольку в логике предикатов в предложениях допускается наличие переменных, то для нахождения контрарных пар требуется введение операции унификации (подстановки константы вместо переменной в предикаты, имеющие одинаковые предикатные символы, но разные литеры). Алгоритм унификации разработали в 1966 г. Ж. Питра и независимо от него – Дж. Робинсон: чтобы унифицировать два различных выражения, отыскивается наиболее общий унификатор – НОУ (подстановка, при которой выражение с большей описательной мощностью согласуется с выражением, имеющим малую описательную мощность). Наличие этого алгоритма позволило реализовать метод резолюций Эрбрана в виде программы для ЭВМ.
Итак, если требуется методом резолюций доказать истинность какого-либо логического утверждения, то отрицание этого утверждения преобразуется в клаузальную форму, по его предложениям выполняется поиск пустого предложения с использованием унификации и вывода резольвент. Невыполнимость отрицания подтверждает истинность рассматриваемого утверждения.
Метод резолюций получил широкое распространение из-за высокой эффективности машинной обработки. На его основе построен язык «Prolog». Однако человек в процессе рассуждений такой логикой не пользуется, и это дает основание для поиска более естественных для человеческого сознания процедур вывода заключений.
Существенным недостатком метода резолюций является то, что он предназначен только для доказательства теорем. Он не пригоден для порождения новых предложений. К тому же, если предложение не является теоремой, резолюция может привести к построению бесконечного дерева решений.
Пример: вывод решения в логической модели на основе метода резолюций.
Даны утверждения:
- «Сократ – человек»;
- «Человек – это живое существо»;
- «Все живые существа смертны».
Требуется методом резолюций доказать утверждение «Сократ смертен».
Решение:
Шаг 1. Преобразуем высказывания в дизъюнктивную форму:
Шаг 2. Запишем отрицание целевого выражения (требуемого вывода), т.е. «Сократ бессмертен»:
Шаг 3. Cоставим конъюнкцию всех дизъюнктов (т. е. построим КНФ), включив в нее отрицание целевого выражения:
Шаг 4. В цикле проведем операцию поиска резольвент над каждой парой дизъюнктов:
Получение пустого дизъюнкта означает, что высказывание «Сократ бессмертен» ложно, значит истинно высказывание «Сократ смертен».
В целом метод резолюций интересен благодаря простоте и системности, но применим только для ограниченного числа случаев (доказательство не должно иметь большую глубину, а число потенциальных резолюций не должно быть большим). Кроме метода резолюций и правил вывода существуют другие методы получения выводов в логике предикатов.
Источник
