Навигация
Главная
Поиск
Форум
FAQ's
Ссылки
Карта сайта
Чат программистов

Статьи
-Delphi
-C/C++
-Turbo Pascal
-Assembler
-Java/JS
-PHP
-Perl
-DHTML
-Prolog
-GPSS
-Сайтостроительство
-CMS: PHP Fusion
-Инвестирование

Файлы
-Для программистов
-Компонеты для Delphi
-Исходники на Delphi
-Исходники на C/C++
-Книги по Delphi
-Книги по С/С++
-Книги по JAVA/JS
-Книги по Basic/VB/.NET
-Книги по PHP/MySQL
-Книги по Assembler
-PHP Fusion MOD'ы
-by Kest
Professional Download System
Реклама
Услуги

Автоматическое добавление статей на сайты на Wordpress, Joomla, DLE
Заказать продвижение сайта
Программа для рисования блок-схем
Инженерный калькулятор онлайн
Таблица сложения онлайн
Популярные статьи
OpenGL и Delphi... 65535
Форум на вашем ... 65535
HACK F.A.Q 65535
Бип из системно... 65535
Гостевая книга ... 65535
Invision Power ... 65535
Пример работы с... 65535
Содержание сайт... 65535
Организация зап... 65535
Вызов хранимых ... 65535
Создание отчето... 65535
Программируемая... 65535
Эмулятор микроп... 65535
Подключение Mic... 65535
Создание потоко... 65535
Приложение «Про... 65535
Оператор выбора... 65535
Модуль Forms 65535
ТЕХНОЛОГИИ ДОСТ... 62923
Имитационное мо... 58297
Реклама
Сейчас на сайте
Гостей: 6
На сайте нет зарегистрированных пользователей

Пользователей: 13,091
новичок: avegraf
Новости
Реклама
Выполняем курсовые и лабораторные по разным языкам программирования
Подробнее - курсовые и лабораторные на заказ
Delphi, Turbo Pascal, Assembler, C, C++, C#, Visual Basic, Java, GPSS, Prolog, 3D MAX, Компас 3D
Заказать программу для Windows Mobile, Symbian

Моделирование информационно-поисковой библиографической системы на gpss ...
Диплом RSA, ЭЦП, сертификаты, шифрование на C#
Выбор наилучших альтернатив с использованием методов оптимизации на Delp...

Реклама



Подписывайся на YouTube канал о программировании, что бы не пропустить новые видео!

ПОДПИСЫВАЙСЯ на канал о программировании
Этап 6 - выделение множества дизъюнктов


Формула, имеющаяся к началу этого этапа, в общем случае представляет совокупность конъюнктивных членов, являющихся литералами или состоящих из литералов, соединенных дизъюнкцией. Давайте сначала рассмотрим структуру формулы на верхнем уровне, не вникая в детали организации конъюнктивных членов. Формула могла бы иметь, например, следующий вид:
(А &В) & (С & (D &Е))



где переменные обозначают, возможно, сложные высказывания (формулы), но при этом они не содержат внутри конъюнкций. На данном этапе нет никакой необходимости знать структуру вложенности, представляемую использованием скобок, так как все высказывания
(А &В) & (С & (D  & Е)) А  & (( В&С) & (D  & Е)) (А &В) & ((С  & D)  & Е )



обозначают одно и то же. И хотя структурно эти формулы различны, они имеют один и тот же смысл. Это объясняется тем, что если установлена истинность всех высказываний из некоторого множества, то не имеет значения каким образом они группируются в сложное конъюнктивное высказывание. Не имеет значения, например, как сказать « А истинно и В и С также истинны» или « А и В истинны и С тоже истинно». Следовательно, скобки никак не влияют на смысл формулы. Можно просто написать (неформально):
A & B & C & D & E



Далее, порядок записи этих формул также не имеет значения. Безразлично, как сказать: « А и В истинны» или « В и А истинны», так как оба эти высказывания имеют одно и то же значение. И наконец, нет необходимости указывать знак конъюнкции (&) между формулами, так как заранее известно, что на верхнем уровне формула является конъюнкцией составляющих ее частей. Поэтому, в действительности, значение представленной формулы можно выразить значительно короче, представив ее в виде совокупности {А, В, С, D, Е} . Название «совокупность» подчеркивает, что порядок элементов не имеет значения. Совокупность {А, В, С, D, Е} в точности то же самое, что и {В, А, С, Е, D} , {Е, D, В, С, А} и так далее. Формулы, являющиеся элементами совокупности, полученной в результате преобразования некоторой формулы исчисления предикатов, называются дизъюнктами. Таким образом, каждая формула исчисления предикатов эквивалентна (в некотором смысле) совокупности дизъюнктов.
Давайте рассмотрим несколько подробнее, что представляют собой эти дизъюнкты. Как уже было сказано, они состоят из литералов, соединенных друг с другом с помощью дизъюнкции. В общем случае, дизъюнкт выглядит примерно так:
((V # W) # X) # (Y # Z)



где переменные являются литералами. Теперь те же самые рассуждения, которые были сделаны о структуре формулы на верхнем уровне, можно применить к дизъюнктам. Как и выше, скобки не влияют на значение дизъюнкта. Точно так же несуществен и порядок литералов. Таким образом, можно просто сказать, что дизъюнкт – это совокупность литералов (неявно соединенных дизъюнкцией). В последнем примере это будет {V, W, X, Y, Z}
Теперь исходная формула представлена в стандартной форме. Более того, использовавшиеся для преобразования правила не зависят от того, существует или нет интерпретация, при которой формула истинна. Стандартная форма состоит из совокупности дизъюнктов, каждый из которых представляет совокупность литералов. Литерал – это либо атомарная формула, либо отрицание атомарной формулы. Эта форма является достаточно лаконичной, так как в ней опущены логические связки конъюнкций, дизъюнкций и кванторы всеобщности. Но при этом, очевидно, следует помнить о принятых соглашениях. И каждый раз, имея дело со стандартной формой, понимать, где и что в ней опущено. Рассмотрим, что представляет собой стандартная форма некоторых формул (предполагается, что уже выполнены первые пять этапов преобразования). Прежде всего вернемся к уже рассматривавшемуся примеру:
(выходной(Х) # работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))



Эта формула порождает два дизъюнкта. Первый дизъюнкт содержит литералы:
выходной(Х), работает(крис,Х)



а второй литералы:
выходной(Х), сердитый(крис), унылый(крис)



Другой пример. Формула
(человек(адам)&человек(ева))&
((человек(Х) # ~мать(Х,Y)) # ~человек(#))



дает три дизъюнкта. Два из них содержат по одному литералу каждый
человек (адам)
и
человек (ева)
Другой содержит три литерала:
человек(Х), ~мать(Х,Y), ~человек(Y)



В заключении этого раздела рассмотрим еще один пример, демонстрирующий все этапы приведения формулы к стандартному виду. Начнем с формулы
all(X, аll(Y,человек(Y) -› почитает(Y,Х) -› король(Х))



утверждающей, что, если все люди относятся с почтением к некоторому человеку, то этот человек является королем. (Для каждого X , если каждый Y является человеком, почитающим X , то X – это король). После устранения импликации (этап 1) получаем:
аll(Х,~(аll(Y,~человек(Y) # почитает(Y,Х))) # король(Х))



Перенос отрицания внутрь формулы (этап 2) приводит к следующему:
аll(Х,ехists(Y,человек(Y) & ~почитает(Y,Х)) # король(Х))



Затем, в результате сколемизации (этап 3) формула преобразуется к виду:
аll(Х,(человек(f1(Х)) & ~почитает(f1Х),Х)) # король(Х))



где f1 -сколемовская функция. Теперь производится удаление кванторов всеобщности (этап 4), что приводит к формуле;
(человек(f1(X)) & ~почитает(f1(Х),X)) # король(Х)



Затем формула преобразуется к конъюнктивной нормальной форме (этап 5), в которой конъюнкция не появляется внутри дизъюнктов:
(человек(f1(Х) # король(Х)) & (~почитает(f1(Х), X) # король(Х))



Эта формула содержит два дизъюнкта (этап 6). Первый дизъюнкт имеет два литерала:
человек(f1(Х)), король(Х)



а второй дизъюнкт имеет литералы:
почитает(f1(Х),Х), король(Х)



Опубликовал Kest July 10 2009 12:26:57 · 0 Комментариев · 6183 Прочтений · Для печати

• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •


Комментарии
Нет комментариев.
Добавить комментарий
Имя:



smiley smiley smiley smiley smiley smiley smiley smiley smiley
Запретить смайлики в комментариях

Введите проверочный код:* =
Рейтинги
Рейтинг доступен только для пользователей.

Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.

Нет данных для оценки.
Гость
Имя

Пароль



Вы не зарегистрированны?
Нажмите здесь для регистрации.

Забыли пароль?
Запросите новый здесь.
Поделиться ссылкой
Фолловь меня в Твиттере! • Смотрите канал о путешествияхКак приготовить мидии в тайланде?
Загрузки
Новые загрузки
iChat v.7.0 Final...
iComm v.6.1 - выв...
Visual Studio 200...
CodeGear RAD Stud...
Шаблон для новост...

Случайные загрузки
Самоучитель PHP 4
Создание оригинал...
ICQ
Экранная лупа
SUIPack
Fig [Исходник на ...
Советы по Delphi
Программа рисует ...
AID антивирус
Delphi 6. Учебный...
PDF
PBFoldder
Книга по Delphi (...
Пример создания W...
Керниган Б.В., Ри...
TmxOutlookBarPro
EditButton
Архив Апгрейтов с...
ComboBox97
iComm v.6.1 - выв...

Топ загрузок
Приложение Клие... 100476
Delphi 7 Enterp... 87817
Converter AMR<-... 20082
GPSS World Stud... 13428
Borland C++Buil... 12045
Borland Delphi ... 8665
Turbo Pascal fo... 7048
Visual Studio 2... 5005
Калькулятор [Ис... 4900
FreeSMS v1.3.1 3545
Случайные статьи
Отчет об ошибках: ...
Вообразите какого-...
Тестирование
Практический Перл ...
Функция GetSystemI...
Практическая реали...
Функция InstallUse...
Кому адресована эт...
Краткий обзор пото...
Точность подачи ко...
Класс TJPEGImage
Программирование в...
Определение типа д...
Проблемы синхрониз...
Я преподаю этот ме...
Доступ к объектной...
Стандарт XPath
NonPOD-типы
Коды, исправляющие...
Легенда ждет вас -...
Доступ к аргумента...
Старые открытки
В здании несколько...
Два хоста обменива...
Пакет android.net.sip
Статистика



Друзья сайта
Программы, игры


Полезно
В какую объединенную сеть входит классовая сеть? Суммирование маршрутов Занимают ли таблицы память маршрутизатора?