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

Упорядоченный линейный вывод в ЛППП.

Читайте также:
  1. III. Выводы
  2. III. Выводы
  3. III. Выводы или резюме
  4. VI. Вычислить криволинейный интеграл.
  5. Боли при поражении почек и мочевыводящих путей
  6. Была ли она русской или она была таки еврейской, делать выводы вам, читатель.
  7. В отличие от почек, которые выводят с мочой из организма преимущественно ней­тральные соли, кожа способна выводить сами кислоты.

Будем считать, что литеры в клозе упорядочены. Для того чтобы сохранять информацию об отрезанных литерах, они не удаляются, а только обрамляются. Если на каком-то шаге получается клоз, содержащий две одинаковые литеры, то оставляется самая левая из них, после чего отбрасываются все обрамлённые литеры, за которыми не следуют необрамлённые. Эта операция называется отождествлением влево. Если в упорядоченном клозе последняя литера унифицируется с отрицанием одной из обрамлённых литер, то клоз называется редуцируемым и производится его редукция, то есть:

1) удаляется последнюю литеру и обрамленную литеру, с отрицанием которой унифицируется последняя литера;

2) отбросываются все обрамлённые литеры, за которыми не следуют необрамлённые.

Например, pÚqÚsÚùq

qÚsÚùq

p

//Пример переделать под ЛППП (14)

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

{b/x}

P (b) Ú Q (b, f(b)) Ú S (y) Ú ù Q (b, f))

P (b)

Упорядоченной бинарной резольвентой (упорядоченной резольвентой) клозов C1 и C2, содержащих контрарные литеры L1 и L2 (причем L1 – последняя литера в клозе C) называется клоз C вида C={C1¢}È{C2/L2}, где C1¢ получен из С1 путём обрамления последней литеры.

Например, pÚq

ùqÚr

pÚqÚr

//пример переделать под ЛППП (15)

{b/x} P (x) Ú Q (x, f (a))

ùQ (b, a) Ú R (z)

P (b) Ú Q (b, f (a)) Ú R (z)

Упорядоченным линейным выdодом (OL-выводом) пустого клоза из S (OL-опровержением множества S) называется вывод, удовлетворяющий следующим условиям:

1) отрезаемая литера всегда последняя;

2) вывод имеет следующий вид:

 

//cхему подправить (12 – аналогично)

 

где Сi - центральные клозы, Вj - боковые. Боковой клоз всегда выбирается либо из входного множества, либо среди клозов, полученных на предыдущих шагах. Клоз C называется верхним в выводе.

OL-вывод является так называемой почти полной стратегией.

Теорема о полноте OL-вывода. Если множество клозов S противоречиво, а множество {S/C} - выполнимо, где C S, то существует OL-вывод пустого клоза из S с верхним дизъюнктом C.

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

 


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


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

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