Процесс доказательства методом резолюций.

Используется доказательство методом от противного. Отрицание заключения принимается в качестве дополнительной посылки.

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

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

При необходимости применяются законы де Моргана:

Процесс доказательства методом резолюций. - student2.ru .

2. Все полученные в 1–м пункте дизъюнкты записываются с новой строки (включая отрицание заключения). В результате получается последовательность формул или последовательность дизъюнктов.

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

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

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

Преимущества использования правила резолюций:

1) В этом методе используется лишь одно правило – это правило резолюций. Не надо запоминать многочисленные правила вывода и теоремы классического исчисления высказываний.

2) В процессе доказательства не надо использовать различные равносильности для проведения простых преобразований.

3) Метод прост в реализации.

Замечание. На основе этого правила разработан язык логического программирования – Пролог.

Пример. Процесс доказательства методом резолюций. - student2.ru . Доказать выводимость.

Процесс доказательства методом резолюций. - student2.ru

1) Процесс доказательства методом резолюций. - student2.ru ; Процесс доказательства методом резолюций. - student2.ru ;

2) Процесс доказательства методом резолюций. - student2.ru – гипотезы

Дизъюнкты: 1. Процесс доказательства методом резолюций. - student2.ru ;

2. Процесс доказательства методом резолюций. - student2.ru ;

3. Процесс доказательства методом резолюций. - student2.ru ;

4. Процесс доказательства методом резолюций. - student2.ru ;

5. Процесс доказательства методом резолюций. - student2.ru ;

3) 6. Процесс доказательства методом резолюций. - student2.ru (2, 4)

7. Процесс доказательства методом резолюций. - student2.ru (3, 5)

8. Процесс доказательства методом резолюций. - student2.ru (1, 6)

9. Процесс доказательства методом резолюций. - student2.ru – ложь.

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

5. ЛОГИКА ПРЕДИКАТОВ

5.1. Определение предиката

Понятие предиката обобщает понятие высказывания, а логика предикатов представляет собой дальнейшее развитие логики высказываний.

Предикат – предложение, похожее на высказывание, но все же им не являющееся: о нем нельзя судить истинно оно или ложно. Дадим определение предиката.

Определение 1. n–местным предикатом, заданным на множестве М1´М2´…´Мn называется выражение, содержащее n переменных x1, х2, ..., хn, которое становится высказыванием при подстановке вместо этих переменных элементов а1, а2, ..., аn, из множеств М1, М2, ..., Мn соответственно.

Предикаты обозначаются как Р(х1, х2, ..., хn) и пред­ставляют собой отображения Р: М1´М2´…´Мn Процесс доказательства методом резолюций. - student2.ru {0,1}. То есть, упорядоченному набору элементов (а1, а2, ..., аn) из множества М1´…´Мn ставится в соответствие один из элементов множества {0,1}, причем 0, если Р(а1, а2, ..., аn) – ложное высказывание и 1, если истинное. Переменные х1, х2, ..., хn называются предметными, а элементы из множеств М1, М2, …, Мn, которые эти переменные пробегают – конкретными предметами. Местностью предиката называется число различных аргу­ментов, от которых зависит предикат. Предикат является функцией многих переменных.

Примеры

1. Предложение "х – четное число" представляет собой од­номестный предикат, заданный на множестве целых чисел, то есть Р: Z®{0, 1}. Областью определения предиката Р является множе­ство целых чисел Z, областью значений – множество {0, 1}.

2. Отношения "х < у" и "х делится на у"представляют собой двуместные предикаты, заданные на множествах R´R и Z´Z соответственно.

Определение 2. Множеством истинности предиката Р(х1, х2, ..., хn), заданного на множестве М1´М2´…´Мn, называется совокупность таких упорядоченных наборов элементов (а1, а2, ..., аn) из М1´М2´…´Мn, для которых высказывание Р(а1, а2, ..., аn) является истинным.

Обозначение: P+ ={(а1, а2, ..., аn): l( Р(а1, а2, ..., аn)) =1}.

Примеры.

1. Множеством истинности двухместного предиката Р(х, у):"х делится на у", заданного на множестве М´М,
где М = {1, 2, 3, 4, 5, 6}, является следующее множество Р+ = {(1,1), (2,1), (3,1), (4,1), (5,1), (6,1), (4, 2), (6, 2), (6,3)}.

2. Множество истинности двуместного предиката Р(х,y): "x < у", заданного на множестве М1´М2, где М1 = {1, 2, 3}, М2 = {2, 4, 6}, равно P+ = {(1,2), (1,4), (1,6), (2,4), (2,6), (3,4), (3,6)}.

Определение 3.Два предиката Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn), за­данные на одном и том же множестве М1´М2´…´Мn, называются равносильными, если оба предиката принимают истинные значения на одних и тех же наборах (а1, а2, ..., аn) из множества М1´М2´…´Мn, то есть, если Р+= Q+. Предикат Q(х1, х2, ..., хn), заданный на множестве М1´М2´…´Мn называется следствием предика­та Р(х1, х2, ..., хn), заданного на том же множестве, если он становится истинным высказыванием при всех значениях переменных х1, х2, ..., хn из соответствующих множеств М1, М2, ..., Мn, при кото­рых истинным высказыванием становится предикат Р(х1, х2, ..., хn), то есть, если Процесс доказательства методом резолюций. - student2.ru .

5.2. Логические операции над предикатами

Определение 4. Отрицанием предиката Р(х1, х2, ..., хn), заданного на множестве М1´М2´…´Мn, называется новый предикат Процесс доказательства методом резолюций. - student2.ru1, х2, ..., хn), заданный на том же множестве, который становится истинным высказыванием при таких значениях (а1, а2, ..., аn) из множества М1´М2´…´Мn, при которых Р(а1, а2, ..., аn) является ложным высказыванием и становится ложным высказыванием, если Р(а1, а2, ..., аn) является истинным высказыванием.

Например, отри­цанием одноместного предиката Р(х): "х делится на 3", заданного на множестве М = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} будет предикат Процесс доказательства методом резолюций. - student2.ru : "х не делится на 3". Множествами истинности предикатов Р и Процесс доказательства методом резолюций. - student2.ru яв­ляются следующие множества Р+= {0, 3, 6, 9}, ( Процесс доказательства методом резолюций. - student2.ru )+ = {1, 2, 4, 5, 7, 8}.

Множество истинности предиката Процесс доказательства методом резолюций. - student2.ru является дополнением множества Р+,то есть Процесс доказательства методом резолюций. - student2.ru ( M – область определения предиката).

Определение 5. Конъюнкцией двух n–местных предикатов Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn), заданных на множестве М1´М2´…´Мn, называется новый n–местный предикат Р(х1, х2, ..., хn) Процесс доказательства методом резолюций. - student2.ru Q(х1, х2, ..., хn), который становится истинным высказыванием только для таких элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn, для которых Р(а1, а2, ..., аn) и Q(а1, а2, ..., аn) являются истинны­ми высказываниями.

Определение 6. Дизъюнкцией двух n–местных предикатов Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn), заданных на множестве М1´М2´…´Мn, называется новый n–местный предикат Р(х1, х2, ..., хn) Ú Q(х1, х2, ..., хn), который становится ложным высказыванием только для таких элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn, для которых Р(а1, а2, ..., аn) и Q(а1, а2, ..., аn) являются ложными высказываниями.

Определение 7. Импликациейдвух n–местных предикатов Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn), заданных на множестве М1´М2´…´Мn, называется новый n–местный предикат Р(х1, х2, ..., хn) Процесс доказательства методом резолюций. - student2.ru Q(х1, х2, ..., хn), который становится ложным высказыванием только для таких элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn, для которых Р(а1, а2, ..., аn) является истинным высказыванием, а Q(а1, а2, ..., аn) является ложным. В остальных случаях – истинным.

Определение 8. Эквивалентностью двух n–местных предикатов Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn), заданных на множестве М1´М2´…´Мn, называется новый n–местный предикат Р(х1, х2, ..., хn) Процесс доказательства методом резолюций. - student2.ru Q(х1, х2, ..., хn), который становится истинным высказыванием только для таких элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn, для которых высказывания Р(а1, а2, ..., аn) и Q(а1, а2, ..., аn) ли­бо одновременно являются истинными, либо ложными. В остальных случаях – ложным.

Если предикаты Р(х1, х2, ..., хn) и Q(y1, y2, ..., ym) заданы на разных множествах, то в результате применения операций конъюнк­ции, дизъюнкции, импликации и эквивалентности к этим предика­там, получим (n + m – k)–местный предикат, где k – число переменных, общих для обоих предикатов.

Кванторные операции

Кроме операций отрицания, конъюнкции, дизъюнкции, им­пликации и эквивалентности в логике предикатов имеются две кванторные операции: квантор всеобщности( Процесс доказательства методом резолюций. - student2.ru ) и существования( Процесс доказательства методом резолюций. - student2.ru ). Если Р(х) одноместный предикат, заданный на некотором множестве М, то в результате применения кванторов к предикату Р(х) получим новые предикаты Процесс доказательства методом резолюций. - student2.ru P(x) и Процесс доказательства методом резолюций. - student2.ru Р(х), означающие соот­ветственно "все х из М обладают свойством Р"и "некоторые х из М обладают свойством Р".

Пример 1.Пусть Р(х) одноместный предикат "х делится на 7", за­данный на множестве целых чисел Z. Применяя к этому предикату кванторы получим следующие предикаты: "все х из Z делятся на число 7" и "существуют х из Z, которые делятся на число 7". То есть, в результате применения кванторов ( Процесс доказательства методом резолюций. - student2.ru ) и ( Процесс доказательства методом резолюций. - student2.ru ) к одномест­ному предикату Р(х)получили высказывания, причем первое из них ложное, а второе – истинное. Высказывания являются нульместными предикатами.

Применение кванторов к предикатам понижает местность исходного предиката на единицу. Если Р(х1, х2, ..., хn) n–местный предикат, то в результате применения кванторов получим новые предикаты Q(х2, ..., хn)= Процесс доказательства методом резолюций. - student2.ru Р(х1, х2, ..., хn), R(х2, ..., хn)= Процесс доказательства методом резолюций. - student2.ru Р(х1, х2, ..., хn), которые зависят только от переменных х2, х2, ..., хn,то есть являются (n – 1)–мест­ными предикатами.

Предметная переменная, которая связывается квантором, то есть входит в предикат и в квантор, называется связанной. Предметная переменная, не связанная никаким квантором, называется свободной переменной.

Пример 2.Пусть Р(х, y)двухместный предикат, заданный неравенством "х2 + у2 Процесс доказательства методом резолюций. - student2.ru 1" на множестве R´R. Множеством истинности преди­ката Р(х, y)является множество всех точек координатной плоскости, расположенных внутри окружности радиуса 1, включая точки ок­ружности. Найдем множества истинности предикатов Q(y)= Процесс доказательства методом резолюций. - student2.ru x P(x, y), R(x)= Процесс доказательства методом резолюций. - student2.ru у Р(х, у), S = Процесс доказательства методом резолюций. - student2.ru x Процесс доказательства методом резолюций. - student2.ru y P(x, y). Множеством истинно­сти предиката Q(y)является множество таких у, для которых данное неравенство выполняется при любых х из R. Однако таких у не су­ществует. Следовательно, множество истинности предиката Q не со­держит ни одного элемента, то есть Q+ =Æ. Множеству истин­ности предиката R(x)принадлежат все такие х, для которых можно найти число у, удовлетворяющее данному неравенству. Такие зна­чения х лежат в промежутке [–1, 1]. Следовательно, этот промежуток и будет множеством истинности предиката R. Предикат S – нульместный, то есть является высказыванием. В высказывании S говорится, что для любых х можно найти такое у, для которой выполняется данное неравенство. Однако это не верно. Например, для х,лежащих вне отрезка [–1, 1], такое у не существует. Тогда S – ложное выска­зывание.

5.3. Теоретико–множественный смысл предикатов

При определении множества истинности предиката, составленного из нескольких предикатов при помощи логических связок, можно воспользоваться соотношениями для их множеств истинности. Для двух n–местных предикатов Р(х1, х2, ..., хn) и Q(х1, х2, ..., хn) задан­ных на множестве М1´М2´…´Мn, верны следующие соотношения для их множеств истинности:

1) множество истинности отрицания предиката Р равно дополнению множества истинности этого предиката, то есть Процесс доказательства методом резолюций. - student2.ru ;

2)множество истинности конъюнкции двух предикатов Р и Q рав­но пересечению множеств истинности Р+ и Q+, то есть Процесс доказательства методом резолюций. - student2.ru ;

3) множество истинности дизъюнкции двух предикатов Р и Q рав­но объединению множеств истинности Р+ и Q+, то есть Процесс доказательства методом резолюций. - student2.ru ;

4) множество истинности импликации двух предикатов Р и Q равно Процесс доказательства методом резолюций. - student2.ru ;

5) множество истинности эквивалентности двух предикатов Р и Q равно Процесс доказательства методом резолюций. - student2.ru .

Пример. Пусть предикаты Р(х):"х кратно двум" и Q(x): "х кратно трем", заданы на множестве М = {1, 2, 3, 4, 5, 6, 7, 8}. Их множествами истинности являются следующие множества: Р+ = {2, 4, 6, 8}, Q+ = {3, 6}. Тогда, по соотношениям (1)–(5) получим

а) Процесс доказательства методом резолюций. - student2.ru {1, 3, 5, 7}, Процесс доказательства методом резолюций. - student2.ru {l, 2, 4, 5, 7, 8};

б) Процесс доказательства методом резолюций. - student2.ru {3, 6} = {6};

в) Процесс доказательства методом резолюций. - student2.ru = {2, 4, 6, 8} Процесс доказательства методом резолюций. - student2.ru {3,6}= {2, 3, 4, 6, 8};

г) Процесс доказательства методом резолюций. - student2.ru ={1, 3, 5, 7} Процесс доказательства методом резолюций. - student2.ru {3,6} ={1, 3, 5, 6, 7};

д) Процесс доказательства методом резолюций. - student2.ru ={1, 3, 5, 6, 7} Процесс доказательства методом резолюций. - student2.ru {1, 2, 4, 5, 6, 7, 8}= {1,5,6,7}.

5.4. Классификация предикатов

Определение 9.Предикат Р(х1, х2, ... хn), заданный на множестве М1´М2´…´Мn, называется тождественно истинным, если для всех элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn высказывания Р(а1, а2, ..., аn) будут истинными и тождественно ложным, если для всех элементов (а1, а2, ..., аn) из множества М1´М2´…´Мn, выска­зывания Р(а1, а2, ..., аn) будут ложными. Предикат Р(х1, х2, ... хn), за­данный на множестве М1´М2´…´Мn, называется выполнимым, если существует хотя бы один элемент (а1, а2, ..., аn) из множества М1´М2´…´Мn, для которого высказывание Р(а1, а2, ..., аn) будет ис­тинным и опровержимым, если хотя бы для одного элемента (а1, а2, ..., аn) из множества М1´М2´…´Мn высказывание Р(а1, а2, ..., аn) будет ложным.

В соответствии с классификацией предикатов истинность нульместных предикатов, содержащих кван­торы, можно определить следующим образом. Высказывание "x P(x) будет истинным, если предикат Р(х)является тождественно истинным предикатом. В противном случае – ложным. Высказыва­ние $х Р(х) будет истинным, если предикат Р(х) – является выпол­нимым и будет ложным в противном случае.

5.5. Формулы логики предикатов.
Равносильность формул

Определение формулы логики предикатов имеет индуктивный ха­рактер. Сначала задается алфавит символов, из которых составляются формулы:

– предметные переменные: х, у, z, xi, yi, zi ( Процесс доказательства методом резолюций. - student2.ru );

– нульместные предикатные переменные: Р, Q, R, Рi, Qi, Ri,

(i Процесс доказательства методом резолюций. - student2.ru N);

– n–местные ( Процесс доказательства методом резолюций. - student2.ru ) предикатные переменные: Р(, ..., ), Q(, ..., ), R(, ..., ), Рi(, ..., ), Qi(, ..., ), Ri(, ..., ) (i Процесс доказательства методом резолюций. - student2.ru N) с указанием числа свободных мест в них;

– символы логических операций: Процесс доказательства методом резолюций. - student2.ru ;

– кванторы: ", $;

– вспомогательные символы: (, ) – скобки; , – запятая.

Определение 10.(формулы логики предикатов).

1. Каждая нульместная предикатная переменная есть формула.

2. Любой n–местный предикат Р(х1, х2, ..., хn) есть формула.

3. Если F, G – формулы, не содержащие предметных перемен­ных, которые связаны квантором в одной формуле и свободны в другой, то выражения ( Процесс доказательства методом резолюций. - student2.ru ), (F Ù G), (F Ú G), (F ® G ), (F « G) также являются формулами.

4. Если F формула, а х – предметная переменная, входящая сво­бодно в F, то выражения "x F(x) и $x F(x) также являются формулами.

5. Никаких других формул в логике предикатов нет.

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

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

Определение 11.Две формулы F и G называются равносильными, если при подстановке в эти формулы вместо предикатных перемен­ных конкретных предикатов, а вместо предметных переменных конкретных элементов, эти формулы преобразуются в высказывания с одинаковыми логическими значениями, то есть либо оба в ис­тинные высказывания, либо оба в ложные.

Все основные равно­сильности логики высказываний верны также и для формул логики предикатов. Кроме них, в логике предикатов имеются равносильности, связанные с кванторами:

1. Законы отрицания: Процесс доказательства методом резолюций. - student2.ru , Процесс доказательства методом резолюций. - student2.ru .

2. Законы дистрибутивности:

Процесс доказательства методом резолюций. - student2.ru ;

Процесс доказательства методом резолюций. - student2.ru .

3.Если предикат Q не зависит от переменной х, то верны сле­дующие законы:

Процесс доказательства методом резолюций. - student2.ru , Процесс доказательства методом резолюций. - student2.ru ;

Процесс доказательства методом резолюций. - student2.ru , Процесс доказательства методом резолюций. - student2.ru .

4. Законы переименования связанных переменных:

Процесс доказательства методом резолюций. - student2.ru , Процесс доказательства методом резолюций. - student2.ru .

5.Законы перестановки кванторов:

Процесс доказательства методом резолюций. - student2.ru , Процесс доказательства методом резолюций. - student2.ru .

5.6. Классификация формул логики предикатов

Определение 12.Формула F логики предикатов называется выпол­нимой (опровержимой) на множестве М, если можно найти такие конкретные предикаты, заданные на том же множестве, при подста­новке которых вместо предикатных переменных, она преобразуется в выполнимый (опровержимый) предикат. Формула логики преди­катов называется тождественно истинной (тождественно лож­ной) на множестве М, если при подстановке вместо предикатных пе­ременных любых конкретных предикатов, заданных на этом же множестве, она преобразуется в тождественно истинный (тождест­венно ложный) предикат. Формула логики предикатов называется тавтологией (противоречием), если при подстановке вместо преди­катных переменных любых конкретных предикатов, заданных на любом множестве, она преобразуется в тождественно истинный (тождественно ложный) предикат.

Критерием равносильности формул F и G является тавтологичность формулы (F« G).

Пример 1.Вычислить значение формулы Процесс доказательства методом резолюций. - student2.ru , если предикат Процесс доказательства методом резолюций. - student2.ru имеет значение Процесс доказательства методом резолюций. - student2.ru – «число x меньше числа y» и определен на множестве Процесс доказательства методом резолюций. - student2.ru , N= Процесс доказательства методом резолюций. - student2.ru .

Так как при указанном значении предиката Процесс доказательства методом резолюций. - student2.ru высказывание Процесс доказательства методом резолюций. - student2.ru означает утверждение, что «для любого натурального числа x найдется натуральное число y, большее числа x», то это высказывание истинно. Высказывание Процесс доказательства методом резолюций. - student2.ru означает утверждение, что «существует натуральное число x, которое меньше любого натурального числа y». Это высказывание ложно. Поэтому получаем, что исходная формула ложна.

Пример 2. Доказать, что формула Процесс доказательства методом резолюций. - student2.ru выполнима.

Для доказательства выполнимости формулы A достаточно найти область определения двухместного предиката Процесс доказательства методом резолюций. - student2.ru и такое его значение, что в этой области формула принимает истинные значения. Такой областью определения предиката, в частности, будет множество Процесс доказательства методом резолюций. - student2.ru . Действительно, если Процесс доказательства методом резолюций. - student2.ru - предикат «y:x», то формула A тождественно истинна в области М, и, следовательно, выполнима в этой области. Однако, если в качестве предиката Процесс доказательства методом резолюций. - student2.ru взять предикат «y<x», то формула A будет тождественно ложной в области М и, следовательно, невыполнимой в области М. при этом ясно, что формула A не общезначима.

Пример 3. Доказать, что формула Процесс доказательства методом резолюций. - student2.ru является общезначимой.

Считая, что формула A определена на любой области M, проведем равносильные преобразования:

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru

Процесс доказательства методом резолюций. - student2.ru .

То есть формула A тождественно истинна для любых одноместных предикатов Процесс доказательства методом резолюций. - student2.ru и Процесс доказательства методом резолюций. - student2.ru и в любой области.

Пример 4. Доказать, что формула Процесс доказательства методом резолюций. - student2.ru тождественно ложна.

Так как формула Процесс доказательства методом резолюций. - student2.ru , а формула Процесс доказательства методом резолюций. - student2.ru , очевидно, тождественно ложна, то ложна и формула A.

Определение 13.Формула F', равносильная F, называется ее при­веденной формой, если F' из логических связок содер­жит только отрицание, конъюнкцию и дизъюнкцию, а отрицание относится только к предикатным переменным и к высказываниям. Предваренной нормальной формой (ПНФ) фор­мулы F называется такая ее приведенная форма, в которой все кванторы вынесены в начало формулы, а область действия каждого квантора распространяется до конца формулы.

ПНФ – это формула вида Процесс доказательства методом резолюций. - student2.ru , где Процесс доказательства методом резолюций. - student2.ru – один из кванторов " или $ ( Процесс доказательства методом резолюций. - student2.ru ), а формула F не содержит кванторов и является приведенной формой.

Для формул логики предикатов справедлива следующая теорема.

Теорема. Для каждой формулы логики предикатов существует равносильная ей ПНФ.

Предваренные нормальные формы формул в логике предикатов используются для выяснения равносильности формул и для решения проблемы классификации формул.

Одной из задач классификации формул является проблема разрешимости, которая состоит в следующем. Необходимо найти алгоритм, при помощи ко­торого для произвольной формулы логики предикатов можно опре­делить, будет она тавтологией или нет. В отличие от алгебры выска­зываний, для формул логики предикатов общего алгоритма не су­ществует. Это было доказано в 1936 году американским математиком А. Чёрчем. Несмотря на отсутствие алгоритма в общем случае, в неко­торых частных случаях такой алгоритм существует. Например, для формул, содержащих только одноместные предикаты.

6. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ (ИП)

Понятие формулы в ИП вводится так же, как оно вводилось в логике предикатов.

Аксиоматическая теория начинается с выбора системы аксиом. Как и в случае высказываний, этот выбор может быть осуществлен по-разному. Одной из таких систем аксиом может служить система, состоящая из трех аксиом рассмотренного выше формализованного исчисления высказываний и двух дополнительных аксиом (схем аксиом):

(P1) Процесс доказательства методом резолюций. - student2.ru;

(P2) Процесс доказательства методом резолюций. - student2.ru ,

где формула t не содержит свободной переменной x.

К правилу вывода modus pones(MP) добавляются еще два правила вывода:

Процесс доказательства методом резолюций. - student2.ru – правило введения квантора общности ("–правило);
Процесс доказательства методом резолюций. - student2.ru – правило введения квантора существования ( $– правило),

где х не входит свободно в формулу F.

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

Возможны и другие системы аксиом и правил вывода.

Рассмотрим пример вывода в исчислении предикатов.

Пример. Доказать, что

Процесс доказательства методом резолюций. - student2.ru .

Решение.Построим вывод второй формулы из первой:

Процесс доказательства методом резолюций. - student2.ru

Библиографический список

1.Лихтарников Л.М., Сукачева Т.Г. Математическая логика. Курс лекций. Задачник – практикум и решения: Учебное пособие. 3 – е изд., испр. – СПб.:Издательство «Лань», 2008. – 288 с.

2.Дискретная математика: Теория, задачи, приложения / Я.М. Ерусалимский. – 7-е изд. – М.: Вузовская книга, 2005. – 268 с.: ил.

3.Игошин В.И. Задачи и упражнения по математической логике и теории алгоритмов: учеб.пособие для студ. высш.учеб.заведений / В.И.Игошин. – 2-е изд.,стер. –М. : Издательский центр «Академия», 2006. – 304 с.

4.Игошин В.И. Математическая логика и теория алгоритмов: Учеб.пособие для студ. высш.учеб.заведений / В.И.Игошин. –М. : Издательский центр «Академия», 2004. – 448 с.

5.Успенский В.А., Верещагин Н.К., Плиско В.Е. Вводный курс математической логики. – 2-е изд. – М.: ФИЗМАТЛИТ, 2002. – 128 с.

6.Математическая логика и теория алгоритмов. Ч. I: Метод. указания / Казан. гос. технол. ун-т; Сост. А.В.Садыков. Казань, 2005. 48 с.

Содержание

1. ЛОГИКА ВЫСКАЗЫВАНИЙ …….………….…….… 3

1.1. Высказывания и операции над ними …………………3

1.2. Формулы алгебры высказываний …………………… 5

1.3. Классификация формул. Равносильные формулы….. 6

1.4. Нормальные формы ……………………………….....11

1.5. Логическое следование ………………………………18

1.6. Правила вывода ………………………………………21

2. ФУНКЦИИ АЛГЕБРЫ ЛОГИКИ И ИХ ПРИЛОЖЕНИЯ …………………………………………….25

2.1. Функции алгебры логики ……………………………25

2.2. Специальные замкнутые классы функций
алгебры логики ……………………………….…...… 30

2.3. Приложение булевых функций к анализу
и синтезу релейно-контактных схем.................……. 33

3. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ ……..….……… 35

4. ПРАВИЛО РЕЗОЛЮЦИЙ…….………………………41

5. ЛОГИКА ПРЕДИКАТОВ ………………..…….……. 43

4.

5.

5.1. Определение предиката ……………………….……. 43

5.2. Логические операции над предикатами …….……... 45

5.3. Теоретико-множественный смысл предикатов…..…48

5.4. Классификация предикатов …………………….….. 50

5.5. Формулы логики предикатов.
Равносильность формул …………………….……… 50

5.6. Классификация формул логики предикатов……… 52

6. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ ……………….…… 55

БИБЛИОГРАФИЧЕСКИЙ СПИСОК ………………….. 57

Учебное издание

Садыков Айдар Вагизович

Наши рекомендации