Исчисление предикатов

Пусть – произвольное множество. Предположим, что на нем задана тотальная функция (однозначное отображение) на этом множестве : (однозначное отображение), т.е. . Эта функция является -парной (или -местной).

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

Примеры:

1. Пусть – множество целых чисел. Рассмотрим сигнатуру, состоящую из двух бинарных операций: «+», «*». Возникает алгебра чисел – .

2. Задано произвольное множество и операция «*» (или «+»). Получаемая алгебра называется группой.

Частные случаи:

– = , «*» – группа целых чисел.

– (, «+») – группа целых чисел; (2 , «+») – подгруппа группы целых чисел, или группа четных чисел.

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

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

Пример. (2; 4; 10; «+»); 2 + 2 = 4; 2 + 4 = 6 (2; 4; 6; 10; «+») – все то, что можно получить, и является замыканием (все четные числа).

Элементы сигнатуры называются функторами; – терм. Отображение некоторого множества термов во множество {И, Л} называется атомом. Он состоит из двух объектов: , где – предикат, – список термов.

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

Указанием на пункт А или Б являются кванторы: «все» – All: ; «существует» – Exists: .

С помощью кванторов исчисление высказываний обогащается новым типом формул: ; – «И», «Л» в зависимости от .

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

П1 ; П2 ;

MP: : ; : .

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

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

Основные идеи такого приведения:

1. .

Пример. Доказать, что число 36 делится на 6. Вместо этого докажем две другие теоремы: 36/2 и 36/3. После доказательства этих теорем следует, что (36/2) и (36/3) (36/6). Значит, исходную формулу желательно представить в виде конъюнкций.

2. Избавиться от отрицаний перед кванторами:

, .

3. .

Пример. Пусть дана плоскость и вектор нормали.

Высказывание 1: все прямые, лежащие в плоскости, перпендикулярны вектору нормали. Высказывание 2: прямая, лежащая в плоскости, перпендикулярна к вектору нормали (квантор – лишний). Значит, надо стремиться оставить только кванторы , после чего их удалить. Для удаления квантора используют рассуждение Сколема.Сам процесс называется сколемизацией:

.

Алгоритм заключается в выполнении следующих шагов:

Шаг 1. Избавление от импликаций:

.

Шаг 2. «Протаскивание» отрицаний:

.

Шаг 3. Вспомогательная операция – разделение связанных переменных. Основная идея заключается в том, что каждая связанная переменная может встречаться только два раза: первый раз – в обозначении квантора, второй – в обозначении терма:

… … (… …) = … … (… …).

Например, – не имеет смысла; – правильно.

Шаг 4. Приведение к предваренной форме. Основная идея – распространение области действия квантора в наибольшей степени:

,

.

Шаг 5. Сколемизация – избавление от квантора . Вместо квантора появляются произвольные функторы.

Шаг 6. Избавление от квантора (согласно аксиоме ).

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

Шаг 8. Сведение к доказательству предложений – членов конъюнкции. Если каждый из выводов осуществим, то осуществляется вывод всей формулы.

Итак, программирование доказательства теорем сводится к выполнению двух пунктов:

1. Выполнение всех восьми шагов приведения теоремы исчисления предикатов к стандартному виду является работой со стрингами.

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

Дата добавления: 2015-06-04