Метод резолюций

Содержание 

ВВЕДЕНИЕ 

    В автоматическом доказательстве теорем существуют 2 направления: поиск доказательства и поиск следствия .Обе эти программы являются более трудоемкими, чем правило вывода названое методом резолюции, которое Дж.А.Робинсон разработал, опираясь на программы, написанные ранее. Исходя из этого, делаем вывод, что метод резолюции является более актуальным, чем разработанные до этого программы, так как метод резолюции значительно сокращает процесс доказательства теорем в исчислении высказываний.

      Объектом исследования в моей курсовой работе являются методы доказательства тавтологий в теории высказываний.

    Предметом исследования является система изучения метода резолюции и его приложений.

      Цель моей курсовой работы  – ознакомление с методом резолюции  и с программами, осуществляющими поиск доказательств с использованием принципа резолюции.

    Для достижения заданной цели были поставлены следующие задачи:

–      Изучение литературы по теме;

–      Продемонстрировать применение метода резолюции  и решение

        логических задач;

–      Практическая часть-рассмотрение задач на Прологе-языке,    

        построенного на методе резолюции.

    Работа  состоит из введения, основной части, состоящей из четырех глав, и заключения.  
 
 

ГЛАВА 1. МЕТОД РЕЗОЛЮЦИИ В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ И В ИСЧИСЛЕНИИ ПРЕДИКАТОВ ПЕРВОГО ПОРЯДКА.

    Цели  разработки программ для вычислительных машин, способных доказывать теоремы, тесно связаны с проблемой «Искусственный интеллект» и проблемой дедуктивного вывода. Исследователи, работающие в области искусственного интеллекта, придерживаются точки зрения, что доказательство нетривиальных теорем является интеллектуально трудной задачей. В этой главе мы будем изучать программы для доказательства теорем, которые используют аппарат математической логики или, более точно, исчисление предикатов первого порядка. В математической логике можно в довольно удобной форме выразить почти все типы дедуктивных доказательств. Составление программ, доказывающих теоремы на языке математической логики, позволяет исследователям изучать дедукцию в ее наиболее чистом виде. Дедукция важна, поскольку она играет существенную роль при решении многих типов задач (причем не только математических). Программа, доказывающая теоремы, обладает свойством, которое проф. Дж. Маккарти (1959) назвал «здравым смыслом» (соmmоn sense), т. е. способностью делать дедуктивные заключения из заданных фактов. Этот тип здравого смысла является важной составной частью человеческого интеллекта.

    Построение  для вычислительной машины программ, доказывающих теоремы, предусматривает и ряд других целей, связанных с математикой и математической логикой; так, с точки зрения математиков, будущие программы, которые смогут доказывать новые и интересные теоремы, будут весьма полезны сами по себе. Огромным достижением было бы, если бы какая-то программа в будущем смогла доказать или опровергнуть знаменитые теоремы Ферма или Гольдбаха. Математическая логика хорошо подходит для вычислительных машин, поскольку логики в течение многих десятилетий работали над тем, чтобы ее правила вывода стали «механическими». Составление программ, основанных на использовании математической логики, является привлекательной идеей, так как это четко сформулированная и хорошо изученная область математики. Добавим, что составление машинных программ для доказательства теорем полезно и для изучения математической логики. Например, программист может разработать мощные, естественные, интуитивные правила вывода, которые легко затем дополнить эвристиками.

    Среди авторов, написавших программы для  вычислительных машин, способные находить доказательства в логике предикатов первого порядка (называемой также теорией квантификации), можно отметить Р. С. Гилмора (1960), Х. Вана (1965), а также М. Девиса и Г. Путнама (1960). (Грубо говоря, в каждой из этих программ ряд переменных заменяется константными термами, а затем проверяется, не получено ли доказательство теоремы. Если нет, добавляются новые константные термы и делается следующая проверка и т. д.) уже после того как эти программы были составлены, Дж. А. Робинсон (1965) разработал правило вывода, которое он назвал принципом резолюции. Грубо говоря, принцип резолюции выводит из двух заданных утверждений (посылок) наиболее общее возможное заключение; заключение и обе посылки обычно содержат переменные. Принцип резолюции естественнее, интуитивно понятнее и удобнее для использования людьми, чем правила вывода, применявшиеся в предыдущих программах. Более того, принцип резолюции легко дополнить новыми эвристиками. Вслед за этим Вос и др. написали программу, осуществляющую поиск доказательства с использованием принципа резолюции. Полученная программа оказалась более мощной, чем программы, написанные до появления этого принципа. Затем Ли написал программу, отыскивающую следствия, также основанную на использовании принципа резолюции. В следующих разделах этой главы описываются принцип резолюции, программа Воса и др. для нахождения доказательств, программа Ли для отыскания следствий и делаются соответствующие выводы. 

1. ПРИНЦИП РЕЗОЛЮЦИИ.

    Принцип резолюции представляет собой правило вывода. Прежде чем дать его точное определение, мы для иллюстрации различных аспектов этого правила приведем три примера.

    Пример 1. Предположим, что мы хотим, применяя принцип резолюции, найти доказательство нижеследующей теоремы. Предполагается, что логические утверждения справедливы при всех значениях входящих в них переменных; например, утверждение Р1  справедливо для всех х, всех у и всех v в том же самом смысле, в каком равенство х² - у² = (х + у) (х - у) справедливо для всех х и всех у. [Читатель, знакомый с математической логикой, не встретит трудностей при чтении этой главы. Остальным можно порекомендовать, например, превосходную книгу по логике Ст. Клини (1967).]

    Теорема 1. Предположим, что:

P1. Если  х есть часть v и  если v есть часть у, то х есть часть у.

Р2. Палец  есть часть кисти руки.

Р3. Кисть  руки есть часть руки.

Р4. Рука есть часть человека.

    Анализируя  все четыре посылки Р1 - Р4, мы должны заключить, что палец есть часть  человека.

    Доказательство  теоремы 1. Процедура, с помощью которой осуществляется поиск доказательства с использованием принципа резолюции, сначала формирует отрицание доказываемого утверждения, а затем пытается вывести противоречие. В данном примере отрицанием доказываемой теоремы будет следующее утверждение:  

Р5. Палец  не есть часть человека.

    Резольвентой  Р1 и Р2 будет:

Р6. Если кисть руки есть часть у, то палец есть часть у.

    Р6 является следствием из посылок Р1 и  Р2. Термин резольвента здесь определен на примере; более точное определение будет дано ниже. Р6 получается в результате «взаимной подгонки» (отождествления) предложения Р2 и первой части предложения Р1 путем замены х на «палец» и замены v на «кисть руки». Эта подстановка в Р1 дает следующий промежуточный результат, который является логическим следствием из Р1:

Р1´. Если палец есть часть кисти руки и  кисть руки есть часть у, то палец есть часть у.

    Это выражение в самом деле является логическим следствием из Р1, так как Р1 истинно для всех х и всех v (и для всех у), а поэтому истинно и в частном случае, когда х есть «палец», а v - «кисть руки». Предложение Р6 является непосредственным следствием из Р1' и Р2. Обычно резольвенту Р6 получают непосредственно, минуя промежуточный результат P1'.

    Каждая  из трех частей предложения Р1 называется атомарной формулой. Например, второй атомарной формулой в Р1 является выражение «v есть часть у». Каждое из предложений Р2, Р3 и Р4 состоит из одной атомарной формулы. Р6 состоит из двух атомарных формул.

    Возвращаясь к доказательству, сопоставляем предложение Р3 и первую атомарную формулу в предложении Р6, заменяя в Р6 «у» словом «рука». Это дает промежуточный результат:

Р6'. Если кисть руки есть часть руки, то палец  есть часть руки.

Это предложение  вместе с Р3 дает резольвенту 

Р7. Палец есть часть руки.  
 
 
 
 

Таблица 1. Доказательство теоремы 1 

    Подобным  же образом резольвента, получаемая путем отождествления Р7 и первой атомарной формулы предложения Р1, есть:

Р8. Если рука есть часть у, то палец есть часть у.

    Из  Р4 и первой атомарной формулы  предложения Р8 получаем резольвенту 

    Р9. Палец есть часть человека.

Отождествляющая подстановка для  полученного  предложения Р9 и предложения Р5 приводит к противоречию, что и завершает доказательство теоремы 1.

    Это доказательство в общих чертах приведено  в первой и второй колонках табл. 1. В этой таблице соответствующее доказательство, записанное в символической форме, ясно само по себе, за исключением следующего. Выражение r [РЗ, Р6а] обозначает резольвенту, полученную при соответствующей отождествляющей подстановке для предложения РЗ и для первой атомарной формулы в предложении Р6. Символ ^ обозначает «и». Символ → обозначает «если ... , то ... », или «импликацию». Символ ─ обозначает «не».

    Пример 2. Принцип резолюции состоит из разложения и резолюции. Этот пример иллюстрирует разложение, дизъюнктивную запись и способ формулирования теоремы при применении принципа резолюции. Для понимания ключевых идей принципа резолюции читателю, не знакомому с абстрактной алгеброй, следует все же прочитать этот раздел.

    Теорема 2. В любой ассоциативной системе, в которой имеются левое и правое решения s и t для всех уравнений s · x = у и x · t = у, существует правый единичный элемент.

Доказательство. Ниже приведены замечания по поводу записи формулировок первых четырех предложений из табл.2.

А1. Существование левого решения. Это означает, что для всех х и для всех

    у     существует такое  s, что s · x = у. Другими   словами, существует

    такая функция g(x, у) = s, то g(x, у) ∙ х = у.

А2. Существование правого решения. Это означает, что  для   всех х и   для

        всех у существует  такое t, что x · t = у. Другими  словами,   существует     

        такая функция h(x,y) = t, что x · h(x, у) = у.

АЗ. Ассоциативность. Это    означает,  что (х · y)· z=x ·(у ·z).    Фактически

    нам   необходимо и в дальнейшем  используется  только     следующее      

    выражение: ( х · у=и) ^ (y · z=v) ^ (x · v=w) →(и · z = w).

А4. Отрицание заключения (доказываемого утверждения).

    В данном случае это означает, что  не существует правого единичного элемента.

Таблица 2. Доказательство теоремы 2. 

Иначе говоря, для любого предполагаемого  правого единичного элемента х справедливо существование такого u, что u · х ≠ u. Другими словами существует функция k(x) = и, такая, что k(x)·x ≠k(x).

В доказательстве, приведенном в табл.2, предложение А5 получается из предложения АЗ путем «разложения» АЗ относительно первой и третьей атомарных формул. Предложение АЗ влечет за собой частный случай А5, причем А5 называется множителем АЗ. Этот множитель находится в результате определения отождествляющей подстановки для первой атомарной формулы х · у = u и третьей атомарной формулы x · v =w  предложения АЗ. Это делается заменой всюду в АЗ v на у и w на u и вычеркиванием третьей атомарной формулы, которая становится аналогом первой (а поэтому излишней). В общем случае разложение предложения относительно двух и более атомарных формул выполняется следующим образом:

    А. Находится минимальная подстановка (если она существует), которая делает атомарные выражения идентичными (что понимается под минимальной подстановкой будет разъяснено ниже).

    Б. Найденные подстановки делаются во всем предложении, и затем вычеркиваются все аналогичные атомарные формулы, кроме одной.

    Пример 2 используется также для иллюстрации импликации и дизъюнкции. Представление x ∙ у = z через Р(х, у, z) преобразует

    Чтобы проиллюстрировать минимальную  подстановку, попытаемся разложить  на множители следующее предложение относительно первых двух атомарных формул:

    Р (f (w), w)  V P (у, g (х))V Р (w, f (у).

Попытаемся  найти подстановку, делающую идентичными  две атомарные формулы, двигаясь слева направо. Первой необходимой  подстановкой является замена у на f(w). [Разумеется, обратная замена f(w) на у не справедлива.] Замена у на f(w) во всем предложении приводит к

Р (f (w), w) V Р (f (w), g (х)) V Р (w, t (f (w))).

Следующей необходимой подстановкой будет  замена w на g(x). [Неминимальная подстановка h(z) вместо х и gh((z)) вместо w также приводит к тождественности атомарных формул, но разложение, полученное таким образом, было бы частным случаем и поэтому хуже разложения, которое мы получим.] Подставляя g(x) вместо w, получаем

Р (f (g (х)), g (х)) V Р (f (g (х)), g (х)) V

V Р (g (х), f (f (g (х)))).

Таким обrазом, подстановка в исходное предложение  g(x) вместо w и f(g(x)) вместо у является минимальной. Множитель, полученный вычеркиванием одной из двух идентичных атомарных формул, имеет вид

Р (f (g (х)), g (х)) V Р (g (х), f (f (g (х)))).  

Таблица 3. Запись доказательства теоремы 2 на языке символической логики(исчисления предикатов) 

    Пример 3. Пример, приведенный в табл. 4, иллюстрирует принцип минимальной подстановки при резолюции. Списки аргументов В1 и В2 можно сделать тождественными с помощью минимальных подстановок. Каждый из списков аргументов приобретает вид

s, g (s), m (g (s)), h (s, m (g (s))), n (g (s), h (s, m(g (s)))), k (s, m(g (s)), n(g (s), h (s, m (g (s))))).  
 

Таблица 4. Иллюстрация принципа минимальной подготовки в резолюции.

    Процедура резолюции, впервые описанная в  статье Дж. А. Робинсона (1965), приводит к  доказательству уже в результате одного простого вычисления, которое  можно проделать вручную за несколько  минут. Процедуре, указанной им в более ранней статье, пришлось бы проделать 10^256 подстановок ,прежде чем она   привела бы к противоречию.  

1.2ТОЧНОЕ  ОПРЕДЕЛЕНИЕ ПРИНЦИПА  РЕЗОЛЮЦИИ.

    Определим теперь более точно принцип резолюции (или резолюции и разложения). Определение мы выразим в терминах дизъюнктивной записи.

Грубо говоря, принцип резолюции сочетает в себе следующие две идеи:

1. Принцип силлогизма в пропозициональном исчислении. Этот принцип устанавливает, что из a V b ─ а V с можно заключить, что b V с.

2. Принцип отыскания частных случаев в исчислении предикатов.Этот принцип устанавливает, что от формулы F(v1, v2,… , vn) (которая по предположению справедлива для всех значений входящих в нее переменных v1, v 2,… , vn) можно перейти к формуле F(t1, t2, … , tn) путем подстановки «термов» t1, t2, ... , tn  соответственно вместо переменных v1, v 2,… , vn . По определению термами могут быть:

1)индивидуальная константа, например «палец»;

2)индивидуальная переменная, например х ;

3)функция других термов, например g(x, у) и h(s, m(g(s))).

    Поясним теперь понятие общей (фундаментальной) резолюции (часть принципа резолюции). (Дизъюнктивное) предложение состоит из дизъюнкции литер. Па определению литера является атомарной формулой или отрицанием атомарной формулы. Резольвента (если она существует) литеры одного предложения и литеры другого предложения является следствием двух этих предложений, рассматриваемых совместно. Резольвента получается следующим образом:

    А. Переменные переименовываются таким  образом, чтобы все индивидуальные переменные в одном предложении отличались от  всех индивидуальных  переменных в другом предложении.

    Б. Находится минимальная подстановка, если таковая существует, которая  делает литеры одинаковыми, но  противоположными «по знаку».

    В. Выполняется подстановка повсеместно в обоих предложениях.

    Г. Если после подстановки одна и  та же литера входит в предложение  более чем один раз, в этом предложении  вычеркиваются все одинаковые литеры кроме одной.

    Д. Вычеркиваются две литеры, которые стали одинаковыми, но имеют противоположные знаки.

    Е. Резольвента есть дизъюнкция литер, оставшихся в первом предложении, и  литер, оставшихся во втором предложении.

    Рассмотрим  теперь общее разложение (часть принципа резолюции). Множитель, если он существует, от двух или более литер предложения есть следствие этапа предложения. Множитель получается следующим образом:

    А. Находится минимальная подстановка, если таковая существует, которая  делает литеры одинаковыми (и с теми же самыми знаками).

    Б. Выполняется подстановка повсеместно  в предложении.

    В. Вычеркиваются все, кроме одной, литеры, которые оказались одинаковыми  в результате подстановки.

    Г. Множитель есть дизъюнкция оставшихся литер.  

    1.3 ЭФФЕКТИВНОСТЬ, ПРАВИЛЬНОСТЬ  И ПОЛНОТА ПРИНЦИПА РЕЗОЛЮЦИИ.

     Дж. А. Робинсон (1965) впервые показал, что принцип резолюции является эффективной, правильной и, в отношении поиска доказательства, полной процедурой. Р. Ли (1967) впервые доказал, что правила резолюции является полным и в применении к отысканию следствий. Эффективность принципа резолюции означает, что при его использовании можно написать программу. В самом деле, Вос и сотр., Ли и другие исследователи написали такие программы и работали с ними. Правильность принципа резолюции означает, что из каждого предложения логически следует каждый из его множителей и что из всяких двух предложений логически следует каждая из их резольвент. Та, что принцип резолюции является правильной процедурой, должно быть ясна внимательному читателю.