Доказательство от противного

4.2 Доказательство от противного

4.2.1 Неаксиоматическое описание процедуры

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

Пусть в качестве å задана группа логических формул следующего вида:

Отец(x, y) : x является отцом y;

Брат(x, y) : x, y – братья;

Кузен(x, y) : x, y – двоюродные братья;

Дедушка(x, y) : x – дедушка y.

Используя эти предикаты можно записать следующие утверждения:

(1) ("x1)("y1)("z1)((отец(x1, y1) Ù отец(y1, z1)) ® дедушка(x1, z1)):

если x1 отец y1, а y1 отец z1, то x1 дедушка z1.

(2) ("x2, y2, z2, w2)((отец(x2, y2) Ù брат(x2, z2) Ù отец(z2, w2)) ® кузен(y2, w2)) .

(3) ("x3, y3, z3)((отец(x3, y3) Ù отец(x3, z3) Ù ) ® брат(y3, z3)).

Предположим также, что помимо этих логических формул заданы следующие факты:

(4) Отец(Александр, Сергей),

(5) Отец(Сергей, Ричард).

(6) Отец(Сергей, Иван).

Сначала неаксиоматически зададим процедуру, которая из логических формул выводит заключение. Вывод формулы C из логических формул A, B будем задавать в виде схемы:

А: Все люди смертны

В: Сократ – человек

С: Сократ – смертен.

Если в переменную подставляется значение, то слева от наклонной черты запишем имя переменной, а справа – значение. Например, если в переменную x подставляется значение Сократ, то будем это записывать как x/Сократ.

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

Например, предположим, что задан вопрос: «Кто дедушка Ричарда?». Его можно записать в виде:

($x)(дедушка(x, Ричарда)).

Ответ может быть получен в следующей последовательности:

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

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

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

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

4.2.2 Процесс нормализации

4.2.2.1Префиксная нормальная форма

Рассмотрим фразу «любой человек имеет отца». Ее можно представить в логике предикатов в следующем виде:

("x)(человек(x) ® ($y)(отец(y, x))).

$ находится внутри ППФ. Это не всегда удобно, поэтому целесообразно вынести все кванторы за скобки, чтобы они стояли перед ППФ. Такая форма носит название префиксной нормальной формы.

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

Во-первых, необходимо исключить связки ® и ». По определению:

Следовательно, во всех комбинациях ППФ можно ограничиться тремя связками Ú, Ù и ` .

Предикат, не содержащий переменных, аналогичен высказыванию, поэтому такие предикаты будем обозначать F, G. Когда некоторое выражение выполняется для любого квантора " и $ будем записывать такой квантор Q.

Легко показать:

1.

Это соответствует: высказывание не имеет отношения к квантору переменной, которая включена в другой предикат.

Между предикатами существует следующее соотношение:

Таким образом, «необязательно F(x) выполняется для всех x» º «существует такое x, что F(x) не выполняется»; «не существует такое x, что выполняется F(x)» º «для всех x не выполняется F(x)».

Далее имеем:

2.("x)F(x)Ù("x)H(x) = ("x)(F(x)ÙH(x))

 ($x)F(x)Ú($x)H(x) = ($x)(F(x)ÚH(x)).

Это означает, что квантор " обладает дистрибутивностью относительно Ù, а $ - относительно Ú.

С другой стороны:

("x)F(x)Ú("x)H(x)¹("x)(F(x)ÚH(x)).

($x)F(x)Ù($x)H(x)¹($x)(F(x)ÙH(x)).

Это легко показать. Пусть для первого выражения x определен на множестве D ={а, б, в}, при этом истиной являются F(а), F(б), H(в). Тогда левая часть не выполняется, а правая истинна. На самом деле справедливо:

("x)F(x)Ú("x)H(x)®("x)(F(x)ÚH(x)).

($x)F(x)Ù($x)H(x)®($x)(F(x)ÙH(x)).

Смысл этих формул в том, что описание для двух разделенных предикатов не совпадает с описанием, использующим эти предикаты одновременно как одно целое и с одинаковыми переменными. Поэтому, изменив все переменные в их правых частях, получим:

("x)F(x)Ú("x)H(x) = ("x)F(x) Ú ("y)H(y),

($x)F(x) Ù($x)H(x) = ($x)F(x) Ù ($y)H(y).

Теперь H(y) не содержит переменной x и поэтому не зависит от связывания x. Отсюда:

3. ("x)F(x)Ú("x)H(x) = ("x)("y)(F(x) Ú H(y)),

($x)F(x) Ù($x)H(x) = ($x)($y)(F(x) Ù H(y)).

Таким образом, процесс получения префиксной нормальной формы можно представить как последовательность шагов:

1.   Используя формулы для ®, », заменим их на Ù, Ú, ¾.

2.   Воспользовавшись выражениями

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

3.   Вводятся новые переменные, где это необходимо.

4.   Используя 1, 2, 3 получаем префиксную нормальную форму.

В качестве примера рассмотрим следующее выражение:

Шаг1:

Шаг2:

Шаг 3: нет необходимости.

Шаг 4: используем выражение 1 по переменной z –

Теперь применяем выражение 1 по переменной w –

Похожие работы

Общая терминология программирования

Скачать

71422

1

0

... программирование [application programming] — разработка и отладка программ для конечных пользователей, например бухгалтерских, обработки текстов и т. п.   Системное программирование [system programming] — разработка средств общего программного обеспечения, в том числе операционных систем, вспомогательных программ, пакетов программ общесистемного назначения, например: автоматизированных систем ...

Программирование и достижения компьютерной техники

Скачать

60551

0

0

... разработки программ, но и разработку пакетов прикладных программ. Эти разработки должны обеспечивать высокое качество и вестись примерно так же, как и выпуск промышленной продукции. Достижения компьютерной техники   1.         Универсальные настольные ПК Что такое настольный компьютер, объяснять никому не надо — это любимое молодежью устройство, чтобы красиво набирать тексты рефератов, а ...

Графические возможности программирования в курсе информатики

Скачать

110612

10

19

... набор процедур и функций языков программирования Basic и Pascal, позволяют управлять графическим режимом работы экрана, создавать разнооборазные графические изображения и выводить на экран текстовые надписи. ГЛАВА 2. ГРАФИЧЕСКИЕ ВОЗМОЖНОСТИ ЯЗЫКА ПРОГРАММИРОВАНИЯ В КУРСЕ ИНФОРМАТИКИ БАЗОВОЙ ШКОЛЫ (НА ПРИМЕРЕ BASIC И PASCAL)   2.1 Разработка мультимедиа курса «Графические возможности языков ...

Функциональное и логическое программирование

Скачать

11287

1

10

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