47097 (588464), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

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

2. Подход к программе с позиций потока данных. Такой взгляд на программу уместен, когда известна природа выходного потока (то есть множество ответов). При программировании реализуется такая внутренняя структура программы, которая создает желаемый выходной поток. Если важен порядок следования ответов в выходном потоке, то при построении программы следует в явной форме учитывать процедурные факторы.

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

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

1.2 Основные механизмы дедукции

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

Прямая цепочка рассуждений предполагает использование правил для логического вывода новых фактов, а также фактов, которые имплицитно существовали ранее, но могут быть сделаны явными посредством применения правил. То есть механизм вывода работает для пополнения изначального запаса истинных фактов фактами, которые подразумеваются посредством набора правил. Подобная прямая цепочка рассуждений на практике неприменима: в системе с реальным числом правил имеется столь много подразумеваемых (скрытых) фактов, что, будучи обнаружены, они затмят те несколько фактов, которые действительно представляют интерес и являются полезными.

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

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

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

Механизм вывода на Прологе основан на обратной цепочке рассуждений. Процесс выполнения программы сводится к установлению истинности определенного предложения в Прологе (и обычно в определении величин определенных переменных в процессе) посредством обратной цепочки рассуждений и продолжается до тех пор, пока не будут найдены некоторые базовые истинные факты, известные системе.[3]

1.3 Исчисление предикатов как язык для решения задач

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

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

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

Мы обычно пользуемся языком для того, чтобы делать утверждения, касающиеся интересующей нас области. Отношения между языком и описываемой им областью определяется семантикой этого языка. Правильно построенные формулы исчисления предикатов как раз являются теми выражениями, которые мы будем использовать в качестве утверждений, касающихся интересующей нас области. Говорят, что правильно построенные формулы принимают значения T или F в зависимости от того, являются эти утверждения в этой области истинными или ложными. Приемы обращения с правильно построенными формулами позволяют строить умозаключения, относящиеся к некоторой области, и, следовательно, могут представить интерес при создании принятия решения, требующего такого умозаключения.[2]

1.3.1 Унификация и принцип резольвенции в исчислении

предикатов

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

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

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

В общем случае любую подстановку можно представить в виде множества упорядоченных пар Пара означает, что повсюду переменная заменяется термом . Существенно, что переменная в каждом ее вхождении заменяется одним и тем же термом. Для получения частных случаев литерала были использованы четыре подстановки

Обозначим через частный случай литерала P, получающийся при использовании подстановки . Например, . Композицией двух подстановок и называется результат применения к термам подстановки с последующим добавлением пар из , содержащие переменные, не входящие в число переменных из . Можно показать, что применение к литералу P последовательно подстановок и дает тот же результат, что и применение подстановки , то есть . Можно также показать, что композиция подстановок ассоциативна: . Если подстановка применяется к каждому элементу множества литералов, то множество соответствующих ей частных случаев обозначается через . Множество литералов называется унифицируемым, если существует такая подстановка , что . В этом случае подстановку называют унификатором , поскольку ее применение сжимает множество до одного элемента. Наиболее общим (или простейшим) унификатором для будет такой унификатор , что если - какой-нибудь унификатор для , дающий , то найдется подстановка , для которой .

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

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

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

Принцип резольвенции непротиворечив и полон. Непротиворечивость означает, что если когда-нибудь мы придем к пустому предложению, то исходное множество обязано быть неудовлетворимым. Полнота означает, что если исходное множество неудовлетворимо, то, в конце концов, мы придем к пустому предложению.[2]

1.3.2 Методы поиска доказательства в исчислении предикатов

1.3.2.1 Исчисление предикатов при решении задач

Иногда достаточно только знать, следует ли логически правильно построенная формула W из некоторого множества S правильно построенных формул. Если W не следует из S, то, возможно, мы захотим знать, следует ~W из S. Конечно, в силу неразрешимости исчисления предикатов не всегда можно установить, следует ли W из S.

Характеристики

Список файлов ВКР