Онтология - лекции

( v1) ( v2) ( v3) v1 + v2 = v3 & v2 > 0 (v1 > v3)

Исключение знака импликации из формулировки теоремы дает следующее предложение

( ) ( ) ( ) углы(, , ) ( > / 2 & > / 2)

В результате преобразований отрицания теоремы получаем три конъюнкта

1)углы( *, *, *), где *, * и * - константы Сколема,

2)* > / 2

3)* > / 2

Преобразование аксиом дает следующие конъюнкты

4)углы(, , ) > 0

5)углы(, , ) + + =

6)(v1 > v3) (v2 > v4) v1 + v2 > v3 + v4

7)(v1 > v2 / 2 + v2 / 2) v1 > v2

8)(v1 + v2 = v3) (v2 > 0) (v1 > v3)

Вывод пустого дизъюнкта

9)* > 0, (1 и 4) = (*, *, *),

10)* + * + * = , (1 и 5) = (*, *, *),

11)(v2 > v4) * + v2 > / 2 + v4, (2 и 6) = (v1 *, v2v2, v3

/2, v4v4),

12)* + * > / 2 + / 2, (3 и 11) = (v2 *, v4 / 2),

13)* + * > , (12 и 7) = (v1 * + *, v2),

14)(v1 + * = v3) (v1 > v3), (9 и 8) = (v1v1, v2 *, v3v3),

15)(* + * > ), (14 и 10) = (v1 * + *, v3),

16), (13 и 15), = ().

Задание № 15 (по теме "Доказательство теорем")

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

План ответа Формулировка теоремы (содержательная и на языке исчисления

предикатов).

Множество формулировок нелогических аксиом (содержательных и на языке исчисления предикатов).

Вход и его преобразования к первому состоянию порождающего процесса.

Порождающий процесс и вывод.

28. ВЗАИМОСВЯЗЬ МЕЖДУ АЛГОРИТМАМИ И ИСЧИСЛЕНИЯМИ

28.1. Основной вопрос

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

28.2. Алгоритмы - частный случай исчислений

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

В разд. 14 были введены граф-программы, которые являются представительной вычислительной моделью В силу тезиса Чёрча это означает, что любой алгоритм может быть представлен некоторой граф-программой. Граф-программе однозначно соответствует спецификация этой программы. По форме предложения, образующие спецификацию программы, являются правилами некоторого исчисления, заданного в порождающей модели систем реляционных конфлюентных продукций (ср. разд.14 и разд. 22). Легко видеть, что между множеством процессов, описываемых граф-программой, и множеством процессов, описываемых соответствующим ей исчислением, существует взаимно-однозначное соответствие. Отсюда следует, что для любого алгоритма, реализующего некоторую функцию, существует исчисление со входом, реализующее ту же функцию.

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

28.3. Реализация исчислений с помощью алгоритмов

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

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

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

ЛИТЕРАТУРА

1.Бауэр Ф.Л., Гооз Г. Информатика. Вводный курс: В 2-х частях. М:Мир, 1990.

2.Мальцев А.И. Алгебраические системы. М.: Наука, 1970. 302 с.

3.Успенский В.А., Семёнов А.Л. Теория алгоритмов: основные открытия и приложения. М.: Наука, 1987. 288 с.

4.Хоар К. О структурной организации данных // Структурное программирование. М.: Мир, 1975. С. 98-197.

5.Чень Ч., Ли Р.. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. 359 с.

6.Клещев А.С., Артемьева И.Л. Необогащенные системы логических соотношений. Ч.1. // Научно-техническая информация, сер.2.-2000.-№ 7.-С.18-28.