Студопедия — Упорядоченный линейный вывод в ЛППП.
Студопедия Главная Случайная страница Обратная связь

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

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






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

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-10-19; просмотров: 805. Нарушение авторских прав; Мы поможем в написании вашей работы!



Кардиналистский и ординалистский подходы Кардиналистский (количественный подход) к анализу полезности основан на представлении о возможности измерения различных благ в условных единицах полезности...

Обзор компонентов Multisim Компоненты – это основа любой схемы, это все элементы, из которых она состоит. Multisim оперирует с двумя категориями...

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

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

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

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

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

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

Ведение учета результатов боевой подготовки в роте и во взводе Содержание журнала учета боевой подготовки во взводе. Учет результатов боевой подготовки - есть отражение количественных и качественных показателей выполнения планов подготовки соединений...

Сравнительно-исторический метод в языкознании сравнительно-исторический метод в языкознании является одним из основных и представляет собой совокупность приёмов...

Studopedia.info - Студопедия - 2014-2024 год . (0.01 сек.) русская версия | украинская версия