Доказать, что следующие функции вычислимы 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: .

.

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

Полагаем .

Шаг 2: .

.

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

Полагаем .

Шаг 3: .

.

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

Полагаем .

Шаг 4:

Ø.

Вывод: унифицируемо и его НОУ имеет вид

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