Меню
Главная
Авторизация/Регистрация
 
Главная arrow Информатика arrow ИНТЕЛЛЕКТУАЛЬНЫЕ СИСТЕМЫ
Посмотреть оригинал

Prolog и автоматическое доказательство теорем

Логический вывод на основе импликаций

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

В качестве примера рассмотрим для чисел Пеано цель

(1 + 1 = К) и утверждение

Мы должны найти такие значения переменных М, N и Р, для которых

Если не создавать для решения данной задачи специальный алгоритм, первое, что приходит в голову, это интуитивная идея, заключающаяся в том, чтобы установить соответствие каждого аргумента цели с каждым аргументом головы утверждения. Если один из них — переменная, то она должна получить значение аргумента, с которым производится сопоставление. В данном случае устанавливаем М = О, N = р(0) и R = р(Р). Значение Р является неизвестным и R остается переменной. Применяя эти уравнения к телу утверждения, получаем утверждение plus(0, /?(0), Р), которое становится подцелью с другой логической переменной Р. Чтобы достичь данной подцели, мы должны решить уравнение

где правая часть — это правило pz(0 + N = N). Получаем, что N = p(0) иР = р(0).

Данный процесс называется унификацией (unification), и уравнения, которые мы создаем для переменных, представляют собой унификатор {unifier). Процесс унификации имеет несколько скрытых моментов. Один из них заключается в том, что переменные в утверждении (которые на самом деле являются схематическими или метапеременными в продукционном правиле) должны переименовываться, чтобы становиться новыми переменными каждый раз, когда утверждение используется, чтобы разные экземпляры правила не конфликтовали друг с другом. Другой момент может быть проиллюстрирован уравнением N = р(р(М)), которое не имеет решений: правая часть будет иметь на два последователя больше, следовательно, левая и правая части никогда не будут одинаковыми. К сожалению, Prolog не принимает во внимание данную проблему и решает такие уравнения построением циклического терма. Это может проявиться, если мы построим запрос plus(0, Ny p(N))

«Существует ли такое п, чтобы 0 + и = и + 1».

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

 
Посмотреть оригинал
Если Вы заметили ошибку в тексте выделите слово и нажмите Shift + Enter
< Предыдущая   СОДЕРЖАНИЕ   Следующая >
 

Популярные страницы