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

Содержание 

ВВЕДЕНИЕ 

    В автоматическом доказательстве теорем существуют 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