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, N_y p (N))

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

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