Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатика
ИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханика
ОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторика
СоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансы
ХимияЧерчениеЭкологияЭкономикаЭлектроника

Метод резолюции в ЛППП.

Читайте также:
  1. Battement tendu. Методика преподавания, виды.
  2. I. Задачи и методы психологии народов.
  3. II. Метод они должны иметь поистине универсальный, где нужно соблюдать следующее.
  4. III. Методы строительства
  5. IV. Изучите методику объективного обследования.
  6. IV. Методические указания студентам по подготовке к занятию
  7. PEST-аналіз як ефективний метод дослідження макросередовища діяльності підприємства.

Литеры L1 и L2 называются контрарными, если они являются отрицанием друг друга c точностью до унификации (то есть одна из литер изначально является отрицанием другой или ее можно таковой сделать с помощью подстановки).

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

Бинарной резольвентой клозов С1 и С2, содержащих контрарные литеры L1 и L2 назовается клоз C, полученный следующим образом:

С={C1\L1}È{C2\L2}

Примечание. Очевидно, что данное определение аналогично соответствующему определению в логике высказываний.

Примеры.

//примеры - без подстановки и с подстановкой (6)

P (x) Ú Q (x, y) ù P(x) Ú R(z) Q(x, y) Ú R (z) P (x) Ú Q (x, y) ù P(a) Ú R (z) {a/x} Q(a, y) R (z)

 

Доказано, что бинарная резольвента является логическим следствием.

В отличии от ЛВ, в ЛППП различают понятия резольвенты и бинарной резольвенты. Для того, чтобы определить понятие резольвенты необходимо рассмотреть подстановки.

Множество вида /подстановка (7)/ {ti/xi, … tn/xn}, где ti – термы, а xi – переменные называется подстановкой термов ti вместо переменных xi.

Если E – клоз, а Θ – подстановка, то EΘ – подстановочный частный случай, получаемый вследствие замены переменных xi на термы ti.

Пример.

//пример (8)

P (x) Ú Q (f (x), b, y)

{a/x, c/y}

P (a) Ú Q (f (a), b, c)

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

Пусть даны 2 подстановки Θ и Ω. Применим подстановку Θ, а затем подстановку Ω. Тогда будем говорить, что применили композицию подстановок ΩΘ.

Подстановка Θ называется унификатором множества выражений {E1,..,En}, если E1Θ =E2Θ =….=EnΘ.

Подстановка Ω - есть наиболее общий унификатор множества выражений {E1,…,Ek}, если любой унификатор это множества выражений Θ можно получить путем композиции Ω с некоторой подстановкой Ψ. (Θ= ΩΨ).

П. С – дизъюнкт, а Θ - наиболее общий унификатор двух и более его литер, тогда СΘ называется склейкой дизъюнкта С.

Пример.

//пример склейки (9)

P (x) Ú Q (f(x), b, y) Ú P (a)

{a/x)

P (a) Ú Q (f(x), b, y)

Резольвентами дизъюнктов С1 и С2, содержащих контрарные литеры L1 и L2 называются бинарные резольвенты:

A) клозов С1 и С2;

B) любой склейки клоза C1 и клоза С2;

C) клоза С1 и любой склейки клоза С2;

D) любых склеек клоза С1 и С2

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

Примечание. Фактически, вывод сводится к последовательности вычисления бинарных резольвент и склеек.

Пример.

Аксиома 1. Мао Цзедун – человек

Аксиома 2. Все люди смертны.

Теорема. Мао Цзедун – смертен.

//пример формализации и вывода (10)

Вводим предикаты:

C (x) – x - человек

S (x) – x - смертен

Аксиома 1 C (Мао)

Аксиома 2 [C (x) → S (x)] =

Теорема S (Мао)

 

С (Мао) S (Мао)

ù С (x) Ú S (x) {Мао / x}

S (Мао) ù S (Мао)

Здесь также справедлива теорема о полноте резолютивного вывода. Множество клозов S противоречиво, если и только если существует резолютивный вывод пустого клоза из S.

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

Формальный алгоритм незначительно отличается от имеющегося в ЛВ.

ВХОД: S – входное множество клозов.

ВЫХОД: OK – удается получить пустой клоз, NO – не удается.

M:=S; // - M-текущее множество клозов.

while ÏM do

if not Choose (M, C1, C2, p1, p2) then return(NO);

N:=R(M, C1, C2, p1, p2); // - вычисление резольвенты.

M:=M È N; // - пополнение текущего множества.

end

return (OK); //получен пустой клоз

Примечание. Результат функции R здесь множество возможных резольвент клозов С1 и С2, содержащих контрарные литеры р1 и р2.

 


Дата добавления: 2015-09-06; просмотров: 128 | Нарушение авторских прав


Читайте в этой же книге: Введение | Точка зрения Петрунина. | Данные и знания. Основные модели представления знаний | Булева алгебра. | Метод резолюции в ЛВ. | Упорядоченный линейный вывод в ЛППП. | Применение поиска в пространстве состояний при реализации автоматизированного логического вывода. | Логический вывод на хорновских дизъюнктах. | Понятие экспертной системы и применение логического вывода при построении экспертных систем. | Запросы класса C. |
<== предыдущая страница | следующая страница ==>
Основные определения.| Стратегии проведения резолюции.

mybiblioteka.su - 2015-2024 год. (0.007 сек.)