Логическое программирование основывается на представлении задач в виде теорем, доказываемых в рамках исчисления предикатов первого порядка.
Модели и опровержения
В доказательстве теорем стараются показать, что определенная ППФ B есть логическое следствие множества ППП S = {A1, …, An}, называемых аксиомами рассматриваемой задачи. Правило вывод есть правило, при помощи которого из ранее полученных выражений можно получить новое. Например, если Ai и Aj истинные ППФ, то запись:
указывает, что Ak можно получить из Ai и Aj с помощью правила fq. Рассмотрим последовательность S(0), …, S(j+1), образованную из некоторого множества аксиом S по правилу:
S(0) = S,
…
S(j+1) = S(j) È F(S(j),
где F(S) – множество выражений, которое можно получить из множества S, применяя к каждому его элементу все возможные правила fq из конечного множества F={fq}. Говорят, что высказывание B следует из аксиом, принадлежащих S, если B Î S(j) для некоторого j.
Напомним, что терм – это константа, переменная или функция. В качестве своих аргументов n – местная функция должна иметь п термов. Таким образом, термами будут: a, b, c, f(a), g(f(x), y).
Атомом называется предикат со своими аргументами. Литерал – это атом или его отрицание. Предложение C – это дизъюнкция литералов. Множество предложений S интерпретируется как единое высказывание, представляющее конъюнкцию всех его предложений.
Как уже отмечалось, высказывание T следует из множества предложений S, если T есть логическое следствие предложений из S. Предположим для простоты, что T состоит из единственного предложения. Рассмотрим множество предложений:
Для того, чтобы высказывания SÈT были истинными, все предложения Ci и T должны быть истинными. В свою очередь значения истинности этих предложений будут определяться значениями истинности, содержащихся в них атомов, причем значения истинности должны присваиваться атомам так, чтобы, по крайней мере, один литерал в каждом предложении был истинным.
Отдельное присваивание истинности атомам называется моделью. Если S влечет за собой T, то не существует модели, в которой S истинное, а T – нет. Вместе с тем, если высказывание T истинное, то его отрицание должно быть ложным. Поэтому, если S влечет за собой T, высказывание:
(1)
должно быть ложным для любой модели.
Этот же вывод можно сделать следующим образом:
и от противного:
Предположим, что число атомов конечно. Тогда существует конечное множество моделей, так как k атомам можно присвоить логические значения 2k различными способами. Очевидно, что присваивать значения этим комбинациям можно последовательно и если для всех моделей (1) окажется ложным, то, безусловно, S влечет T. Такое доказательство называется методом от противного и составляет основу методов доказательства теорем.
Доказать противоречивость (1), если число атомов конечно, достаточно просто. Просто ли это на практике зависит от количества атомов и от возможности порождать и проверять модели.
Возникает задача выявления условий, гарантирующих конечное число атомов. Пусть S – это множество высказываний истинных для тех атомов, которые непосредственно входят в S и тех, которые из них можно вывести. Последнее множество может быть бесконечным. В этом можно убедиться на следующем примере. Пусть S – высказывание, содержащее единственный атом S = {R(a, x)}.
Предположим, что определена функция g(x). Тогда можем построить бесконечную последовательность R(a, x), R(a, g(x)), R(a, g(g(x))), …. Эта последовательность перечислимая, так как можно придумать схему перечисления, по которой упорядочиваются высказывания. Например, по уровню вложенности второго аргумента. Можно показать, что всегда можно построить схему перечисления бесконечного множества атомов, полученного из конечного при помощи некоторой подстановки.
Предположим, что S не содержит переменных. Такая ситуация называется основным случаем, а соответствующий универсум (область определения) Эрбрановой базой. В основном случае можно провести перечисление.
Докажем, например, для конкретной пары чисел (a, b) (но не для произвольной пары чисел вообще x, y) истинность высказывания:
a = b ® a > b.
Аксиомами будут:
A1: a > b,
A2: a < b,
A3: a = b.
Соответствующие предложения будут иметь вид:
- выполняется одно из отношений;
- одновременно не выполняются никакие два отношения.
В этих обозначениях наше утверждение имеет вид:
и его отрицание A3A1. Отсюда получим:
Обозначим 
Так как в S может быть только 23 = 8 атомарных высказываний, легко построить все возможные модели. Если для каждой из них хотя бы одно предложение в S принимает значение ложь, то высказывание вида (1) будет ложным, и поэтому наше утверждение будет истинным.
| Модель | Предложения, которым присваивается значение ложь |
| A1, A2, A3 | C2, C3, C4 |
| 
|
| C3 |
| 
|
| 
|
| 
|
| 
|
| 
|
Этот метод неэффективен и избыточен. Можно показать, что высказывание S противоречиво, если исследовать меньшее число моделей. Достаточно ограничиться атомами A1 и A3, то есть провести присваивание значений истинности только этим атомам, а значит использовать только четыре модели.
Теорема Эрбрана – Сколема – Геделя. В этой теореме утверждается, что можно найти частичное присваивание, приписывающее значение ложь любому противоречивому множеству предложений.