Метапрограммирование

р v Y и -р v z

где р — высказывание, a Y и Z — формулы исчисления высказываний. В таком случае этап резолюции, выполненный над этими двумя предложениями, приводит к получению третьего предложения:

Y v2

Можно показать, что это предложение логически  следует из двух первоначальных предложений. Поэтому, добавив выражение !Y v Z) к  рассматриваемой формуле, мы не изменим  истинность этой формулы. Таким  образом, в процессе резолюции вырабатываются новые предложения. Если же в конечном итоге будет получено "пустое предложение" (которое обычно обозначается как "nil"), это означает, что обнаружено противоречие. Пустое предложение n i l формируется из двух предложений, имеющих следующую форму:

X И ~Х

Эта форма, безусловно, свидетельствует о противоречии.

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

Рис. 6.1. Доказательство теоремы (a => Ь) i (Ъ => с) => (а "> с) по методу резолюции. Верхняя строка пред- ставляет собой отрицание данной теоремы в форме ис- числения высказываний. Пустое предложение о пижнеп части свидетельствует о том, что отрицание этой тео

ремы  приводит к противоречию

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

Листинг 6.1, Управляемая шаблонами простая программа для доказательства теорем с помощью метода резолюции

После оформления соответствующей конструкции на языке, управляемом шаблонами, получим следующее правило:

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

done( Cl, С2, Р)

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

Правила, приведенные в листинге 6.1, позволяют также учесть некоторые частные случаи, для которых могло бы иначе потребоваться явное представление пустого предложения. Кроме того, имеются два правила, которые упрощают предложения при любой возможности. Одно из этих правил распознает истинные предложения, такие как 

a v b v -а

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

av Ь v a

преобразовав  его в предложение a v b.

Остается нерешенным вопрос о том, как преобразовать заданную формулу исчисления высказываний в форму представления в виде предложений. Эта задача является несложной, и ее выполняет программа, приведенная в листинге 6.2. Процедура translate( Formula} преобразует формулу в множество предложений Cl, C2 и т.д. и вводит эти предложения в базу данных, как показано ниже.

clause I CD .

clause! C2).

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

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

?- translate! -( (a=>b) S (b=>c)=>U=>O) >, run.

Программа в ответ сообщит " Contradiction found" (Обнаружено противоречие), а это означает, что первоначальная формула является теоремой.

 

 

 

 

 

 

 

ЗАКЛЮЧЕНИЕ

 

1. В метапрограммах другие программы рассматриваются как данные. Метаинтерпретатор Prolog представляет собой интерпретатор для языка Prolog на языке Prolog.
2. Можно легко написать метаинтерпретаторы Prolog, которые вырабатывают трассировки выполнения, формируют деревья доказательства и предоставляют другие дополнительные возможности.
3. Обобщение на основе объяснения — это специальный метод компиляции программ. Он может рассматриваться как символическое выполнение программы, управляемое с помощью конкретного примера. Обобщение на основе объяснения представляет собой один из подходов к машинному обучению.
4. Объектно-ориентированная программа состоит из объектов, которые передают друг другу сообщения. Объекты отвечают на сообщения, вызывая на выполнение свои методы. Методы могут быть также унаследованы от других объектов.
5. Программа, управляемая шаблонами, представляет собой коллекцию управляемых шаблонами модулей, которые активизируются при обнаружении шаблонов, имеющихся в "базе данных". Как системы, управляемые шаблонами, могут рассматриваться и сами программы Prolog, Наиболее естественной была бы параллельная реализация систем, управляемых шаблонами, а при последовательной реализации необходимо обеспечить разрешение конфликтов между модулями в конфликтном множестве.
6. В данной работе также реализован простой интерпретатор для программ, управляемых шаблонами, и применен для автоматического доказательства теорем логики высказываний по методу резолюции.

 

 

СПИСОК ЛИТЕРАТУРЫ

 

1. И. Братко. Алгоритмы искуcственного интеллекта на языке Prolog, 3-е издание.
2. У. Клоксин, К. Меллиш. Программирование на языке Prolog.
3. http://ru.wikipedia.org/wiki/%CC%E5%F2%E0%EF%F0%EE%E3%F0%E0%EC%EC%E8%F0%EE%E2%E0%ED%E8%E5