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

 

    Подобным  же образом резольвента, получаемая путем отождествления Р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) впервые доказал, что правила резолюции является полным и в применении к отысканию следствий. Эффективность принципа резолюции означает, что при его использовании можно написать программу. В самом деле, Вос и сотр., Ли и другие исследователи написали такие программы и работали с ними. Правильность принципа резолюции означает, что из каждого предложения логически следует каждый из его множителей и что из всяких двух предложений логически следует каждая из их резольвент. Та, что принцип резолюции является правильной процедурой, должно быть ясна внимательному читателю.