Доказать, что следующие функции вычислимы 3 страница

55.3. Существуют предметы, которые я никогда не вижу.

55.4. Я вижу каждую вещь в некоторый момент времени.

55.5. Если я вижу предмет, то я его тут же беру.

55.6. Если я вижу предмет, то я его беру спустя некоторое время.

55.7. Перед тем, как я беру предмет, я вижу его.

55.8. Если я беру предмет, не видя его до этого, то через некоторое время я вижу его, но не беру.

55.9. Не существует предметов, которые я никогда не беру.

55.10. Я никогда не беру того, что я всегда вижу.

55.11. Всегда существуют вещи, которые я не вижу и не беру.

55.12. Я беру всякую вещь, которую я никогда не вижу.

55.13. Я беру всякий предмет, который я еще не взял до этого.

55.14. Я всегда вижу либо все, либо ничего.

55.15. Если я беру некоторый предмет, который до этого уже видел, то я ранее видел предмет, который взял позднее.

55.16. Некоторые вещи, которые я видел ранее, я всегда вижу вновь спустя определенное время.

55.17. Если я когда-либо видел две вещи одновременно, то в будущем я также увижу их только одновременно.

55.18. Если я когда-либо видел и взял предмет одновременно, то впоследствии я либо делаю то и другое, либо не делаю ни того, ни другого.

ЛАБОРАТОРНАЯ РАБОТА № 6

ЛОГИЧЕСКИЙ ВЫВОД В ИСЧИСЛЕНИИ ПРЕДИКАТОВ

1. ЦЕЛЬ РАБОТЫ

Целью работы является ознакомление с основными формализованными методами доказательства правильности умозаключения в исчислении предикатов.

2. КРАТКИЕ ТЕОРЕТИЧЕСКИЕ СВЕДЕНИЯ

2.1. Метод семантических таблиц

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

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

Таблица 1

Атомарная таблица

Построим семантическую таблицу для формулы .

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

Далее приведена семантическиая таблица для общезначимой формулы.

| |

2.2. Принцип резолюции

2.2.1. Алгоритм унификации

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

Действительно, если мы имеем дизъюнкты типа:

; , то резольвента может быть получена только после применения к подстановки вместо .

В этом случае имеем: ;

Резольвентой этих двух дизъюнктов будет дизъюнкт

А если взять два дизъюнкта

, ,

то никакая подстановка в контрарную пару неприменима и никакая резольвента не может быть образована.

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

Пусть задано множество дизъюнктов

В этом множестве дизъюнктов и - составляющие дизъюнкты.

А выражения ; ; - называются литералами.

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

Подстановочный частный случай литерала получается при подстановке в литералы термов вместо переменных. Пусть имеем литерал . Его частными случаями будут: ;

;

- константный (фундаментальный) случай литерала или атом, так как нет переменных.

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

, здесь подставляется вместо , а вместо ;

;

А теперь переходим собственно к алгоритму унификации.

Пусть имеем дизъюнкты типа:

= ; = .
К этим дизъюнктам резольвента может быть получена только после применения к подстановки вместо и подстановки вместо . Для этого необходимо:

1. Проверить, можно ли применить резолюцию к и

2. Найти подходящую подстановку, допускающую резолюцию.

Такую проверку и вычисление подстановки осуществляет алгоритм унификации.

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

Подстановкой называется конечное множество вида , где - терм, а - переменная, отличная от ( ).

Подстановка называется фундаментальной, если все ( ) являются фундаментальными термами.

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

Рассмотрим применение алгоритма унификации к заданным дизъюнктам и .

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

Для и первым множеством рассогласования будет .

Шаг 2. Для каждой переменной множества рассогласования проверяем, встречается ли она в каком-нибудь другом терме этого же множества.

Шаг 3. Если на предыдущем шаге получен положительный ответ, то дизъюнкты не унифицируемы, и применение алгоритма оканчивается неудачей. Если ответ отрицательный, осуществляем подстановку вместо переменной из множества рассогласования терма из этого множества. Для и применяем подстановку ={x/g(c)}. В результате и принимают вид

= ; .

Шаг 4. Продолжаем двигаться направо, снова выполняя пункты 1-3. Новым множеством рассогласования будет . Применение подстановки дает

= ; .

После этих преобразований можно применить резолюцию к дизъюнктам и .

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

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

Так, например, для для множества

первыми слева различными термами в и являются и . Таким образом, первым множеством рассогласования будет . После применения подстановки возникает несоответствие между термами и . Следующее множество рассогласования . В конце концов, алгоритм заканчивает свою работу, выдавая в качестве ответа множество подстановок, позволяющих унифицировать и , и затем применить к ним правило резолюции для исчисления высказываний. Это Множество подстановок называется общим унификатором (ОУ) дизъюнктов.

Например, для = и = общим унификатором является множество .

Если дизъюнкты не могут быть унифицируемы, алгоритм останавливается на шаге 2

Унификатор называется наиболее общим унификатором (НОУ), если для любого другого унификатора существует подстановка такая, что .

Для множества термов или атомов наиболее общий унификатор определяется единственным способом.

Рассмотрим механизм нахождения НОУ на примере.

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

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

;

Если теперь положить и , то можно показать, что .

Подстановка унифицирует рассматриваемые атомы. Следовательно, является наиболее общим унификатором.

Алгоритм унификации в формальном описании выглядит так. Пусть - множество атомарных формул.

Шаг 0. (тождественная подстановка).

Шаг k. Мы уже построили подстановки .

Шаг (рекурсия).

1) Если = = … = ,

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

2). Если для некоторых , тогда

а) строим множество рассогласования

;

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

Если ПВ дает положительный результат, процесс останавливается и делается заключение, что множество не

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

Шаг . Повторяем шаги , для .

Теорема(Теорема Дж. А. Робинсона) Применение алгоритма унификации к множеству атомов дает следующий результат:

Если унифицируемо, то алгоритм останавливается, выдавая в качестве ответа НОУ множества ;

Если не унифицируемо, то алгоритм останавливается, объявляя, что унификатора не существует.

Воспользуемся теоремами 1 и 2 для определения унифицируемости.

Пример 1. (Множество унифицируемо)

Пусть дано множество формул:

Определить, унифицируемо ли множество . Если да, найти НОУ.

Шаг 0: Полагаем .

Шаг 1: .

ПВ негативна.

Полагаем .