Применение языка SWI-Prolog для автоматического доказательства теорем

Рассмотрим реализацию в среде SWI-Prolog доказательства того, что сумма четных чисел является четным числом. Вполне очевидно, что путем перебора доказать это невозможно, поскольку множество целых чисел бесконечно. Докажем это с помощью прямого логического вывода. Сначала определим, что любое четное число — это число, которое можно представить как произведение некоторого целого числа на 2:

even (X) : — X =_А*2.

В языке Prolog любая переменная, начинающаяся со знака подчеркивания «_», является анонимной; она успешно унифицируется с любым выражением или значением, но при этом ее содержимое для программиста безразлично. Тело вышеуказанного правила означает, что переменная X может быть представлена в виде произведения некоторой величины на 2.

Далее, надо определить правила алгебраических преобразований и, в частности, дистрибутивный закон ab + cb = (а + с) 1 г.

г (X, Y,'Distributive law') X = A*N+B*N,.

Y = (A+B) *N.

Третий аргумент в предикате г необходим для последующего объяснения процесса доказательства. После этого можно задать цель:

?- even (А), even (В), X =А+В, г (X, Y, Law), even (Y),.

writef ('%w:%w — > %w ', [Law, X, Y]) .

Результат будет выглядеть следующим образом:

Distributive law: G262*2+ G265*2 -> (G262+ G265) *2.

Теорема доказана. Результат сложения представлен в виде четного числа. Здесь идентификаторы G262 и _G265 означают свободные переменные.

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

proof (X, Y, [ (RuleName, Y) ]) г (X, Y, RuleName) .

proof (X, Y, [(RuleName, A) |Rest]) г (X, Z, RuleName), proof (Z, Y, Rest) .

Предикат proof возвращает в третьем аргументе список, состоящий из наименования правила и результата, который получен с его помощью. Поскольку машина вывода SWI-Prolog реализует поиск сначала в глубину, существует риск углубления в бесконечные ветви дерева решений. Для устранения бесконечных рекурсий следует исключить повторяющиеся состояния. Для этого заменим обращение к правилу г в предикате proof на следующее правило:

getrule (А, В, Y, RuleName) г (А, В, RuleName),.

+ node (В), assert (node (В)).

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

Программа для поиска алгебраического преобразования X в У выглядит следующим образом:

deep (X, Y): ;

retractall (node (_)),% удаляем все старые узлы.

assert (node (X)),% добавляем исходный узел.

% в список посещенных.

writef ('Given:%w ', [X]),.

writef ('Prove:%w ', [Y]),.

get_time (Tl),.

proof (X, Y, L), % вызов поиска решения printlist (L, 1), writef ('Success '), get_time (T2),.

T is T2-T1, writef ('Elapsed time:%w', [T]), nl.

printlist ([],_).

printlist ([ (Y, L) | Rest], N) writef ('%w%w%w ', [N, Y, L]), N1 is N+l,.

printlist (Rest, N1) .

Попробуем с помощью этой программы выполнить доказательство простейшего преобразования для квадрата суммы двух переменных (а + Ь)² = а² + 2ab + b². Для его реализации наряду с классическими аксиомами, такими как г (X, Y, ' Commutative lawl—') Х = А+В, Y = B+A.

г (X, Y,'Distributive law—') X=A*N+B*N,.

Y = (A+B) *N,.

потребовалось добавить вполне очевидные для человека, но неизвестные для языка Prolog аксиомы:

г (X, Y,' Subtraction to zero-'):^- X = А-А, Y = 0.

г (X, Y,'Doubling rule—X = A+A, Y = 2*A.

г (X, Y,'Adding with zerol—X = A+0, Y = A. г (X, Y, ' Subtraction with zerol'): — X = A-0, Y = A. г (X, Y,'Square rulel—'): — X = A*A, Y = A^A2.

Эти правила задают соответственно тождества А — А — О, А + А = 2А, А + 0 = А, А — 0 = Л, А • А = А². Кроме того, если исходный полином состоит из более чем двух членов, все перечисленные правила не смогут его распознать. Добавим рекурсивное правило для декомпозиции полиномов:

г (X, Y, L) X = A+B, г (A, Al, L), Y = A1+B.

Теперь зададим цель:

?- deep ((a+b) ^л2, а^л2+2*а*Ь+Ь^л2) .

В результате получим:

Given: (a+b) ^л2 Prove: а^/ч2+2*а*Ь+Ь^л2.

• 1 Square rule2—(a+b) * (a+b)
• 2 Distributive law4— a* (a+b) +b* (a+b)
• 3 Commutative lawl—b* (a+b) +a* (a+b)
• 4 Distributive law4— a*b+b*b+a* (a+b)
• 5 Commutative lawl— a* (a+b) + (a*b+b*b)
• 6 Associative law2— a* (a+b) +a*b+b*b
• 7 Commutative lawl—b*b+ (a* (a+b) +a*b)
• 8 Associative law2— b*b+a* (a+b) +a*b
• 9 Commutative lawl— a*b+ (b*b+a* (a+b))
• 10 Commutative law2— b*a+ (b*b+a* (a+b))
• 1318 Commutative lawl— (a+a) *Ь+а^л2+Ь^л2
• 1319 Associative law6— (a+a) *b+ (а^л2+Ь^л2)
• 1320 Commutative lawl— a^A2+b^A2+ (a+a) *b
• 1321 Associative law6 a^A2 + (b^A2+ (a+a) *b)
• 1322 Commutative lawl b^A2+ (a+a) *b+a^A2
• 1323 Commutative lawl— (a+a) *b+b^A2+a^A2
• 1324 Commutative lawl—a^A2+ ((a+a) *b+b^A2)
• 1325 Associative law2— a^A2+ (a+a) *b+b^A2
• 1326 Doubling rule — a^A2+2*a*b+b^A2

Success.

Elapsed time: 2.46 875.

true.

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

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