Интерпретатор языка Пролог (стр. 3 из 15)

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

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

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

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

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

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

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

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

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

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

предикатов

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

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

частными случаями будут , , , .

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

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

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

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

Обозначим через

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

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

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