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

    Принцип резолюции является полным как для нахождения доказательства, так и для отыскания следствий. Напомним, что цель процедуры, которая использует принцип резолюции для нахождения доказательства, состоит в там, чтобы показать, что отрицание подлежащей доказательству теоремы неправомерна (привадит к противоречию). Принцип резолюции является полным для нахождения доказательства в смысле следующей теоремы, впервые доказанной Робинсоном. Если конечное множество предложений несовместно, то противоречие может быть обнаружено за конечное число применений принципа резолюции. Принцип резолюции является полным для нахождения следствий в смысле следующей теоремы, впервые доказанной Р. Ли.

Теорема. Если предложение С является следствием конечного непустого· множества предложений, то за конечное число применений принципа резолюции .может быть найдено предложение Т, такое, что С непосредственно следует из Т.

    Несколько исследователей усилили эти теоремы, показав, что некоторые ограниченные формы принципа резолюции также являются полными. Эта практически важна для автоматического доказательства теорем, потому что теоретические исследования и эксперименты на вычислительной машине показали, что ограниченный, но полный принцип резолюции более эффективен в практических применениях, чем общий (неограниченный) принцип резолюции. Примерами таких ограниченных, но полных форм принципа резолюции является резолюция с «опорным множеством для доказательства геометрических теорем, при котором отбрасываются предположения, сложные относительно заданного геометрического чертежа (модели). За исключением резолюции единичных элементов, которая будет описана в следующем подразделе, дальнейшее теоретическое обсуждение различных ограниченных форм резолюции выходит за рамки данной книги.  

1.4 РЕЗОЛЮЦИЯ ЕДИНИЧНЫХ ЭЛЕМЕНТОВ.

      Резолюция единичных элементов является ограниченной формой резолюции. Она имеет большое практическое значение и используется в настоящее время в наиболее современных программах, доказывающих теоремы. Единичный элемент определяется как предложение, состоящее из одной литеры. Предположим, что сначала находится резольвента единичного элемента U1 с первой литерой другого предложения, а затем находится резольвента единичного элемента U2 с преемником второй литеры этого предложения. Было доказано (Слэйгл, 1967), что этим способом будет получена та же резольвента, которая будет получена, если сначала отыскивается резольвента единичного элемента U2 со второй литерой предложения, а потом U1 с преемником первой литеры предложения. Следовательно, в этом случае резолюция единичных элементов ограничивает резолюцию только одним из двух возможных порядков, в которых может быть получена резольвента.

    В общем случае если имеется  q единичных предложений, которые нужно разрешить с некоторым предложением, то резолюция единичных элементов ограничивает резолюцию одним из q! возможных способов получения резольвенты. Резолюция единичных элементов является частным случаем семантической резолюции, которая при определенных условиях ограничивает резолюцию одним из q! возможных способов, причем U - не обязательно единичные элементы.  

ГЛАВА  2.  СТРАТЕГИИ,      ИСПОЛЬЗУЕМЫЕ          ПРИ ДОКАЗАТЕЛЬСТВЕ ТЕОРЕМ НА ОСНОВЕ ПРИНЦИПА РЕЗОЛЮЦИИ.

    Стратегией  в доказательстве теорем с использованием принципа резолюции является Эвристика, аналогичная порождающей процедуре для деревьев игр. Действительно, стратегия «сначала вширь» аналогична Порождающей процедуре «сначала вширь». Программы для нахождения доказательства или отыскания следствий, основанные на принципе резолюции, должны иметь стратегию (правило) для выбора очередного действия, т. е. для выбора тех предложений и литер, для которых нужно определить множитель или резольвенту. Ниже описаны три стратегии: «сначала вширь», «предпочтение единичным элементам» (unit-ргеfегеnсе) и стратегия «опорного множества». Стратегия «опорного множества» применима только при поиске доказательства, в то время как две другие стратегии могут использоваться в обоих типах доказательства теорем. При нахождении доказательства стратегия включает условие окончания, например наличие противоречия или какой-либо другой критерий окончания.

    Стратегия «сначала вширь» рассматривается нами по трем причинам. Она несложна для  понимания, является основной стратегией, используемой в программе Ли для отыскания следствий, и использовалась Робинсоном в теоретических целях, например в данном им доказательстве полноты принципа резолюции для нахождения доказательств. Стратегия начинается с порождения всех множителей для первоначально заданных предложений. Определяется, что первоначально заданные предложения и их множители имеют уровень О. Исходя из этих предложений нулевого уровня, стратегия порождает уровень 1 путем получения резольвент и множителей этих новых резольвент. Из предыдущих (уровня О и уровня 1) предложений стратегия порождает уровень 2, получая резольвенты и множители этих новых резольвент. Затем стратегия порождает уровень 3 и т. д.

    Стратегия «предпочтение единичным элементам» (Вос и др., 1964) производит дедуктивный  вывод предложений, содержащих возможно меньшее число литер. Одним из преимуществ этой стратегии является то, что короткие предложения легче обрабатывать, чем длинные. Главным же достоинством этой стратегии для нахождения доказательства является то, что предложение, содержащее противоречие, которое программа стремится получить, может рассматриваться как предложение, не состоящее из литер. Хотя эта стратегия не применялась для отыскания следствия, она могла бы оказаться полезной и для этой цели, так как интересные следствия, как правило, коротки. По определению предложение j-гo порядка есть предложение, состоящее из j литер. Таким образом, единичный элемент является предложением 1-го порядка.

    Стратегия «предпочтение единичным элементам», как свидетельствует ее название, дает наивысший приоритет резолюции единичных элементов. Кроме того, эта стратегия приписывает второй по величине приоритет резолюции двух предложений, резольвента которых имеет наименьшее ожидаемое число литер. Ожидаемое число литер для одного предложения h-гo порядка и одного предложения j- гo порядка равно h + j - 2, так как во время поиска резолюции по крайней мере две литеры вычеркиваются. Таким образом, например, стратегия установит следующий порядок нахождения резольвент: единичный элемент с единичным элементом, единичный элемент с предложением 2-го Порядка, единичный элемент с предложением 3-го порядка, единичный элемент с предложением 6-го порядка, затем предложение 2-го порядка с предложением 3-го порядка, предложение 3-го порядка с предложением 4-го порядка, предложение 2-го порядка с предложением 6-го порядка и т. д.

    Стратегия «предпочтение единичным элементам» начинает с поиска резольвент единичного элемента с единичным элементом. Например, в табл. 5 процедура поиска доказательства с использованием этой стратегии пытается, но безуспешно, сопоставить Р2 и Р3.  

    Таблица 5.Стратегия «предпочтение единичным  элементам» 

    Далее она пытается доказать попарно идентичность четырех элементов от Р2 до Р5, но не достигает успеха. Следующей ее попыткой является сопоставлен

      полной в следующем смысле. Если аксиомы правомерны (логически совместны), то противоречие (предполагается, что оно существует) может быть найдено за конечное число шагов; при этом не допускаются резольвенты каких-либо двух аксиом (или их множителей). В табл. 6 предложение Р5 является единственным предложением, входящим в опорное множество.

    Стратегия «опорного множества» не будет пытаться подбирать для разрешения пары литер из аксиом P1-P4. 
 
 
 

Таблица 6.Стратегия  «опорного множества»(предполагается, что Р5-единственное предложение ,составляющее опорное множество литер) 

ГЛАВА 3. ПРОГРАММА, ИСПОЛЬЗУЮЩАЯ ПРИНЦИП

РЕЗОЛЮЦИИ ДЛЯ НАХОЖДЕНИЯ ДОКАЗАТЕЛЬСТВ.

    Вос и др. (1964) составили программу  для нахождения доказательств с  использованием принципа резолюции. На самом деле они предложили несколько программ, но мы  опишем только одну из них. Вначале программа была составлена с использованием процедуры «сначала вширь»,а затем по очереди были введены стратегии «предпочтения единичным элементам», «опорного множества» и резолюция единичных элементов. По мере того как вносилось каждое из этих изменений, действие программы последовательно улучшалось. В то время как для доказательства одной теоремы при использовании стратегии «сначала вширь» требовалось 30 мин, при использовании стратегии «предпочтение единичным элементам» на одну теорему затрачивалось уже менее 1 с. По затратам машинного времени и объема памяти эта программа значительно более эффективна, чем программы для нахождения доказательств  в исчислении предикатов без использования принципа резолюции. Программа сумела найти доказательства ряда значительно более трудных теорем, чем приведенные в трех примерах этой главы. Она находила доказательства теорем как в геометрии, так и в теории чисел. Однако главным образом она применялась для отыскания доказательства первых теорем теории групп в абстрактной алгебре. Вполне возможно, что усовершенствованный вариант этой программы сможет доказать некоторые теоремы, до сих пор еще никем не доказанные.  

ГЛАВА 4. ПРОГРАММА, ИСПОЛЬЗУЮЩАЯ ПРИНЦИП РЕЗОЛЮЦИИ ДЛЯ ОТЫСКАНИЯ СЛЕДСТВИЙ

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

    Для иллюстрации того, как работает программа, предположим, что рассматривается следующая теорема. В ассоциативной системе с левой идентичностью и инверсией слева из существования левой идентичности вытекает и существование правой идентичности. Экспериментатор задает программе первые четыре предложения табл. 7. Целевое следствие есть Р(х, е, х) (предложение С13 в табл. 7). В табл. 7 представлены только те предложения, которые существенны относительно целевого следствия. Программа сначала проверяет предложения С1 и С2. Так как она ожидает, что резольвента будет иметь шесть литер, она не рассматривает эти предложения, поскольку параметр, определяющий верхнюю границу числа литер, равен 4. От предложений C1 и С3 могут быть образованы три резольвенты, однако только одна из них, в которой вычеркнута вторая литера предложения C1, является существенной для порождения целевого следствия. Программа порождает много других предложений на этом уровне, находя резольвенты, скажем C1и С4, С2 и С3 и т. д. Однако в соответствии со стратегией аксиоматической резолюции программа не ищет резольвенты предложений, порожденных одно от другого. Она будет искать резольвенту С5 и аксиомы. Как и ранее, С5 не может дать резольвенту при сопоставлении с C1 или С2, потому что критерий устанавливает число литер, которые должна содержать резольвента. Оно будет сопоставляться с С3 и С4. Затем для получения резольвенты можно сопоставить С6 и С4. Резольвента будет Р(е, е, е)  . Так как это единичное предложение, то Р(е, е, е) Просто-напросто вычеркивается. Этим устанавливается тривиальность следствия предложения С3 и производится его исключение из памяти. Программа рассматривает С9 как первое интересное следствие и добавляет его к аксиомам. Затем программа порождает С10 и признает его интересным. Несколько позже программа порождает С13 и решает, что это предложение интересно. Это и есть целевое следствие.