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


Логика предикатов первого порядка

Сигнатура теории предикатов первого порядка состоит из следующих объектов:

Для записи формул используются логические связки: Кроме связок используются также кванторы: Для конечного предметного множества {a1,a2,...,an} кванторы аналогичны знакам произведения или суммы в обычном анализе:
x P(x) ≡ P(a1) & P(a2) & ... & P(an),           ∃x P(x) ≡ P(a1) ∨ P(a2) ∨ ... ∨ P(an).
Переменная квантора, как и индекс суммирования, является "немой" и может быть переобозначена на любую переменную, которой нет в формуле. Однотипные кванторы перестановочны: xy P(x,y) ≡ ∀yx P(x,y). Различные же кванторы переставлять нельзя. Так, если предикат M(x,y) означает, что "x является матерью y", то xy M(y,x) означает, что "для любого x существует его мать y". Очевидно, что это не эквивалентно утверждению yx M(y,x) ("существует такая y, которая является матерю всех x, включая саму себя").

Если в теории, в качестве стандартного предиката, используется равенство предметных сущностей x=y, то она называется теорией с равенством.


Интерпретация теории

Одна и та-же теория может иметь различные интерпретации. Задание интерпретации означает введение конкретного множества предметных сущностей (конечного или бесконечного) и определение на нём значений объектов сигнатуры теории.

Например, пусть в сигнатуре теории есть предикат P(x,y) и функция f(x).
Введём множество из трёх элементов: X = {a,b,c}.
На этом множестве положим f(a)=b, f(b)=c, f(c)=a и F(a,a)=F, F(a,b)=T,... (9 значений).
Тем самым определена интерпретация теории.

Интерпретаций теории в данной сигнатуре может существовать бесконечно много. Введём следующие понятия:

Правильная формальная теория должна быть непротиворечивой.


Аксиомы мира ящиков

Рассмотрим, в качестве примера, формальную теорию, описывающую прямоугольные закрытые ящики, которые могут находится друг в друге. Сигнатура теории состоит из единственного передиката in(x,y), истинного, если ящик x находится внутри ящика y и ложного в противном случае.

С математической точки зрения отношение in образует строгий древесный порядок. Аксиомы такой теории имеют вид:

1. ∀x    !in(x,x)                                         % антирефлексивность
2. ∀x,y   in(x,y) → !in(y,x)                               % асимметричность
3. ∀x,y,z in(x,y) & in(y,z) → in(x,z)                      % транзитивность
4. ∀x,y,z in(z,x) & in(z,y) → in(x,y) ∨ in(y,x) ∨ x=y      % древесность
Антирефлексивность означает, что сам в себе ящик находиться не может. Асимметричность: если x находится в y, то ящик y не может находиться в x. Транзитивность отношения in допускает вложенность (шкатулка в ящике, ящик в сундуке, поэтому шкатулка и в сундуке). Наконец, древесность запрещает ящику непосредственно находится в двух ящиках одновременно. Если in(z,x) и in(z,y), то это означает, что ящики x и y должны быть вложенными друг в друга (или быть одним и тем же ящиком).

По-мимо аксиом (всегда истинных в данной теории), могут формулироваться факты в которых нет переменных и которые считаются истинными в данной модели (в конкретной ситуации). Например, пусть предметное множество состоит из трёх ящиков {a,b,c} (это константы). И пусть известно, что ящик a находится внутри ящика c и ящик b не находится в ящике c. Эти два утверждения являются фактами:

in(a,c);    !in(b,c).
Из фактов и аксиом можно выводить новые факты. Так, из примера выше следует, что !in(b,a). Однако, если информация об объектах неполна, то не все факты можно вывести (выяснить истинно или ложно данное утверждение). В примере таковым является утверждение in(a,b). Стоит нарисовать две возможные модели расположения ящиков, которые соответствуют фактам in(a,c) & !in(b,c).


Нормальная форма

Перед проведением машинного вывода все формулы представляются в нормальной форме и называются предложениями (clause). В такой форме формулы не содержат кванторов, а предикаты (и возможно их отрицания) соединяются только логическими ИЛИ. Алгоритм приведения к нормальной форме состоит из следующих этапов:

Пример. Пусть предикат H(x) означает, что "x - это человек", а предикат M(x,y) - "x является матерью для y". Сформулируем утверждение: x[ H(x) → ∃y (M(y,x) & H(y))] ("каждый человек имеет мать, которая также человек"). Последовательность действий для получения нормальной формы этой формы имеют вид:

x [ !H(x) ∨ ∃y (M(y,x) & H(y))]                  определение импликации
∀x [ !H(x) ∨ [M(m(x),x) & H(m(x))]]               вводим сколемовскую функцию m(x)
∀x [[!H(x) ∨ M(m(x),x)] & [!H(x) ∨ H(m(x))]       закон дистрибутивности   
    [!H(x) ∨ M(m(x),x)],  [!H(x) ∨ H(m(x))]       опускаем квантор ∀
В результате получаем две формулы в нормальной форме. Первая: !H(x) ∨ M(m(x),x) означает: "если x - человек, то m(x) является его матерью". Вторая: !H(x) ∨ H(m(x)) читается "если x - человек, то значение функции m(x) - тоже человек".


Унификация

При проведении машинного вывода необходимо сравнивать между собой "похожие" формулы. Унификация двух формул - это ниболее общая замена переменных σ, которая делает эти формулы одинаковыми. Если необходимо переменную x заменить на константу a, это обозначается как x/a. Пусть x,y,z,.. - переменые, a,b,c,... - константы. Обычно, переменные при унификации переименовываются таким образом, чтобы в обеих формулах они были различны. Приведём пример унификации формул:

Формула1        Формула2          Замены                     Унификатор
P(z, a),        P(x, y)           σ = {z/x, y/a}             P(x, a)
P(f(x,a), y),   P(z, g(b))        σ = {z/f(x,a), y/g(b)}     P(f(x,a), g(b))
P(a, b),        P(x, c)           σ = ∅                      неунифицируемы
В последнем случае b,c - различные константы и не могут быть заменены друг на друга. Поэтому эти две формулы нельзя сделать одинаковыми.


Вывод по резолюции

Логический вывод формулы F из формул F1,F2,... подразумевает, что всегда, когда истинна F1 & F2 & ..., будет истинной и F. Базовым методом вывода является вывод по резолюции:

A ∨ C,  B ∨ !C     =>    A ∨ B.
Его смысл прост. Мы считаем A ∨ C и B ∨ !C одновременно истинными. Если C ложно, то по первой формуле должно быть истинно A. Если же C - истинно, то !C - ложно и по второй формуле истинным должно быть B. Поэтому, не зависимо от значения C, истинным является или A, или B (или оба). Таким образом, A ∨ B истинно, коль мы считаем истинными формулы A ∨ C и B ∨ !C.

При выводе по резолюции, в двух формулах находят предикат и его отрицание. Они вычёркиваются, а остальные части формул объединяются логическим ИЛИ. Часто, чтобы получить новую формулу, необходимо сначала провести унификацию:

A(x) ∨ C(f(x), a),    B(y) ∨ !C (y, z)   =>   A(x) ∨ C(f(x), a),    B(f(x)) ∨ !C (f(x), a),
откуда выводим A(x) ∨ B(f(x)).

Докажем при помощи резолюции, что аксиома асимметричности следует из аксиом транзитивности и антирефлексивности. Запишем их в нормальной форме и сделаем унификацию подчёркнутых атомов:

!in(x,y) ∨ !in(y,z) ∨ in(x,z),    !in(w,w)  =>  !in(w,y) ∨ !in(y,w) ∨ in(w,w),    !in(w,w).
Теперь по резолюции получаем !in(w,y) ∨ !in(y,w) или in(w,y) → !in(y,w).

Частным случаем вывода по резолюции является вывод modus ponens: A, A → B => B. Действительно, по определению импликации, это эквивалентно A, !A ∨ B => B. Формулы содержат A и её отрицание. Поэтому они "вычёркиваются" и получается B.

Ещё один очевидный вывод делается при помощи подстановки значений переменных. Например, из асимметричности !in(x,y) ∨ !in(y,x) следует антирефлексивность !in(x,x), если заменить y на x.


Прямой вывод

Если в теории нет кванторов существования и не требуется вводить сколемовских функций, то возможен прямой вывод одних фактов из других. Запишем аксиомы мира ящиков в нормальной форме, используя для предиката-отношения in(x,y) операционную форму x in y:

1.  !(x in x)
2.  !(x in y) ∨ !(y in x)
3.  !(x in y) ∨ !(y in z) ∨ (x in z)
4.  !(z in x) ∨ !(z in y) ∨ (x in y) ∨ (y in x) ∨ x=y

Пусть известно, что "ящик a находится внутри ящика c, ящик b не находится внутри ящика c" (факты):

5.    a in c
6.  !(b in c)

Имеем множество из 6 формул. Будем, при помощи резолюции, порождать новые формулы. Так как нас интересуют факты только о предметных константах (конкретных ящиках), будем подвергать резолюции формулы, содержащие хотя бы одну константу. Поэтому, берём 5-ю формулу и проходим сверху-вниз по всем формулам, пытаясь сдедать вывод по резолюции:

7.  !(c in a)                                % res(5,2.1)
8.  !(c in z) ∨ (a in z)                     % res(5,3.1)
9.  !(x in a) ∨ (x in c)                     % res(5,3.2)
10. !(a in y) ∨ (c in y) ∨ (y in c) ∨ c=y    % res(5,4.1)
Выше res(5,2.1) означает резолюцию 5-й формулы с первым атомом 2-й формулы после их унификации. При этом res(5,2.1) и res(5,2.2) дают одно и тоже выражение.

Теперь повторяем вычисления с формулой (фактом) 6:

11. !(b in y) ∨ !(y in c)                    % res(6,3.3)
12. !(z in b) ∨ !(z in c)  ∨ (c in b)        % res(6,4.3)
13. !(b in a)                                % res(6,9.2)
14. !(a in b) ∨ (c in b)                     % res(6,10.3)
Заметим, что в 12, 14 были отброшены заведомо ложные атомы типа b=c. Выведенные формулы с константами, как сложные, типа !(c in z) ∨ (a in z), так и атомарные (факты), типа !(c in a), необходимо снова-сверху вниз применить к списку формул (а также к самим себе). Так как множества констант конечно, эта процедура рано или поздно остановится.

Если в прямом выводе применять резолюцию к двум аксиомам, то будет порождаться бесконечное число формул. В теории выше, это происходит из-за аксиомы транзитивности. Несложно видеть, что по резолюции она, сама с собой приводит к бесконечной цепочке:

!(x1 in x2) ∨ !(x2 in x3) ∨ (x1 in x3),
!(x1 in x2) ∨ !(x2 in x3) ∨ !(x3 in x4) ∨ (x1 in x4),
!(x1 in x2) ∨ !(x2 in x3) ∨ !(x3 in x4) ∨ !(x4 in x5) ∨ (x1 in x5),
...


Метод грубой силы

Иногда предметное множество конечно и требуется получить истинность всех выражений которые не содержат переменных. Тогда можно использовать следующий простой алгоритм. В каждую аксиому последовательно подставляются все возможные значения переменных из предметного множества. Атомы, которые в полученных формулах ложны отбрасываются. Например, аксиома транзитивности !(x in y) ∨ !(y in z) ∨ (x in z) в случае трёх предметных констант (ящиков) приведёт к 27 = 3*3*3 формулам. Среди них будет:

!(b in a) ∨ !(a in c) ∨ (b in c).
Если заданы факты (a in c) и !(b in c), то второй и третий атом в формуле являются ложными и так как всё выражение истинно, приходим к истинности факта !(b in a).

Подобная процедура повторяется несколько раз, пока не перестанут получаться новые формулы. Из выведенного множества формул можно, например, отобрать только факты или, при необходимости, короткие утверждения типа: !(a in b) ∨ (c in b).


Вывод от противного

При автоматическом выводе чаще используется не прямой логический вывод, а метод от противного. Он основан на следующей идее. Если из формул {F1,...,Fn} следует формула F, то множество формул {F1,...,Fn,!F} противоречиво. Действительно, логическое следствие означает, что, всегда когда истинно F1 & ... & Fn, должно быть истинным и F (ложным !F). Поэтому F1 & ... & Fn & !F будет ложным.

Противоречие при выводе возникает, когда появляется атом A и его отрицание !A. Поэтому, если необходимо доказать, что формула F истинна, берут её отрицание !F, добавляют к аксиомам и ищут такую резолюцию, которая приводит к пустому предложению: A, !A => ⬜.

Большинство формальных теорий полуразрешимы. Это означает, что если F действительно истинна, то противоречие будет найдено за конечное число шагов (возможно достаточно большое). Если F ложна, то противоречия найдено не будет и алгоритм может не остановиться.

Пусть в примере с ящиками (a in c), !(b in c) и мы хотим доказать, что !(b in a). По сравнению с прямым выводом добавится формула (b in a). Выведенные формулы 7-11 останутся без изменений, а после получения формулы 13: !(b in a) её резолюция с (b in a) приведёт к пустому предложению . В этот момент алгоритм остановится.

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


Простой алгоритм вывода

Рассмотрим пример реального, несколько упрощённого алгоритма машинного вывода на примере документации к системе SPASS. Основной цикл вывода использует следующие правила получения новых формул. В первых двух правилах - σ = unify(C,C') - унификатор атомов C,C':

Строго говоря в Subsumption необходимо также устранять включения формул: A ∨ F, F => F (удаляем A ∨ F).

Пусть на вход алгоритма поступает список предложений L в нормальной форме. Ставится задача вывести из этого списка противоречие (пустое предложение ⬜). Ниже, функциями res, fac, sub, taut обозначены, описанные выше, правила получения (удаления) предложений.

Вначале формируются две очереди open и close. В open помещается исходный список L, который, на всякий случай, "прореживается" методами sub и taut (они возвращают множество предложений):

close  = ∅                               // список уже рассмотренных формул 
open   = taut(sub(L,L))                  // список формул к рассмотрению

while open ≠ ∅ and ⬜ ∉ open {
   F = open.pop()                        // убираем из open формулу F
   close.push(F)                         // помещаем её в close 
   
   N = res(F, close)                     // множество всех резолюций F с формулами из close
   N = N ∪ fac(F)                        // добавляем в него факторизации формулы F
   N = sub(N)                            // убираем повторы
   N = taut(N)                           // убираем тавтологии
   N = sub(sub(N, close), open)          // убираем повторы в N c формулами из close и open
   
   close = sub(close, N)
   open  = sub(open,  N) ∪ N
}

if open = ∅  : print "Completion Found"   
if ⬜ ∈ open : print "Proof Found"   

Основной цикл while повторяется, до тех пор, пока очередь open не опустеет или в ней не обнаружится пустое предложение ⬜. В цикле из очереди open выбирается одна формула F. Выбор определяется некоторыми эвристиками, ускоряющими процесс работы алгоритма. Например, можно брать наиболее короткие формулы (так как мы стремимся получить ⬜), больший вес давать константам и т.д.

Функция res(F, close) порождает все возможные резолюции между формулой F и формулами из списка close. При проведении резолюции между двумя формулами, необходимо переименовать переменные так, чтобы они отличались в обоих формулах. Например, если есть F(x1, x2) и G(x1, x2, x3), то проводится резолюция res(F(x1, x2), G(x3, x4, x5)). В выведенной формуле упорядочивают атомы КНФ и переименовывают переменные (снова в x1,x2,...), чтобы затем проще выполнять функцию sub (удаление одинаковых формул).

Заметим, что если в качестве опровержения используется формула с константами (утверждение о конкретных сущностях), то из open можно извлекать только формулы, содержащие хотя бы одну константу (подправив соответствующим образом условие выхода из while).


Теории с равенством

Если в теории, в качестве стандартного предиката, используется равенство предметных сущностей x=y, то она называется теорией с равенством.

Аксиоматически задавать предикат x=y неудобно. Равенство обладает рефлексивностью: x=x, симметричностью: x=y → y=x и транзитивностью: x=y & y=z → x=z. Кроме этого выполняется: x=y & x=z → y=z. Однако, также необходимо вводить аксиомы типа: x=y → f(x,z) = f(y,x) для каждого предиката и функции сигнатуры.

Вместо этого удобнее использовать дополнительные правила вывода. Формулы с неравенством упрощаются в самом начале. Так, пусть есть формула F(x) ∨ !(x=t), где F(x) - некоторое КНФ выражение, зависящее от переменной x, а t - любой терм (константа, переменная или функция). В формуле можно делать любые подстановки, т.к. её истинность от этого не изменится. Если x=t истинно, то !(x=t) ложно и его можно отбросить. Если же истинно !(x=t), то формула истинна независимо от значения F(x). Поэтому такая формула заменяется на F(t).

Базовый вывод в теории с равеством называется парамодуляцией (ниже t - произвольный терм):

F(a,b),  G(b) ∨ a=t     =>     F(t,b) ∨ G(b)
(если a != t, то истинно G(b), если a = t, то его можно подставить во все формулы). Более сложный пример парамодуляции:
P(g(f(x))) ∨ Q(x),  G(c) ∨  a=f(g(b))     =>    P(g(a)) ∨ Q(g(b)) ∨ G(c)
(в первой формуле сначала делаем подстановку x/g(b), затем повторяем рассуждения).

В общем случае пусть t,r,s - термы, F,G - КНФ формулы и A(t) - атом, зависящий от терма t. Тогда:

A(t) ∨ F,   G ∨ r=s    =>   A(σs) ∨ σF ∨ σG,
где σ - оператор подстановки наиболее общего унификатора для термов t, r.


Смысл сколемизации

В алгоритме приведения к нормальной форме кванторы существования устранялись при помощи введения сколемовских констант и функций. Следует подчеркнуть, что формула после "сколемизции" не эквивалентна формуле до неё. Проще всего показать это на пример. Пусть F: ∃x P(x). Нормальная форма этой формулы имеет вид: F': P(s), где s - сколемовская константа. Введём следующую интерпретацию: множество {a,b} на котором P(a)=F, P(b)=T и s=a. Для этой интерпретации формула F истинна, тогда как F' - ложно.

Тем не менее, если в процессе вывода, с использованием формул F' после сколемизации, возникает противоречие, это означает, что противоречивы и формулы F (до сколемизации). Другими словами F невыполнима тогда и только тогда, когда невыполнима и F'.

Когда есть только сколемовские константы, то это очевидно. Действительно, формула F: ∃x P(x) означает, что существует по меньшей мере одна сущность x=a для которой P(a) истинно. Если ни в какой интерпретации F': F(a) невыполнима, то невыполнима будет и F: ∃x P(x). Аналогичны рассуждения и для сколемовских функций.

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


Теорема Эрбрана

Если множество формул противоречиво, то метод вывода от противного выводит пустое предложение за конечное число шагов. Теоретическим обоснованием этого оптимистического утверждения является теорема Эрбрана.

Пусть, например, в сигнатуре теории (или после сколемизации) есть одна константа a и две функции f(x), g(x). При выводе новых формул проводится их унификация. При этом могут возникать различные константые термы, которые можно упорядочить следующим образом:

{a, f(a), g(a), f(f(a)), g(g(a)), f(g(a)), g(f(a)), .... }
Такое множество предметных констант называется универсумом Эрбрана.

На этом множестве можно задавать различные интерпретации для предикатов, входящих в сигнатуру теории. Пусть в сигнатуре есть два предиката P(x), Q(x). Возможна, например, интерпретация в которой истинны {P(a), !Q(a), !P(f(a)), Q(f(a)), ...}. Все возможные интерпретации можно перечислить при помощи бинарного семантического дерева. Из корневой вершины дерева выходят две ветки. Пусть в левой вершине истинно P(a), а в правой - !P(a). Из каждой вершины снова опустим по две ветки, соответствующих истинности Q(a) и !Q(a), и т.д. При спуске по дереву можно получить любую интерпретацию. Например, приведенная выше имеет путь: влево, вправо, вправо, влево,...

Если универсум Эрбрана бесконечен, то будет бесконечным и семантическое дерево. Однако, если обходить его в ширину, то для каждой вершины будет получаться конечный набор значений предикатов (истина или ложь). Эти значения можно подставить в формулы теории. Если при этом одна из формул окажется ложной, то раскрывать дерево от этой вершины ниже смысла не имеет. Рассмотрим пример противоречивого набора формул:

1. !P(x) ∨ Q(x),  2. P(f(x)) (2),  3. !Q(f(x)) 
Универсумом Эрбрана является множество {a, f(a), f(f(a)), ...}, где a - произвольно введенная константа (хотя бы одна предметная сущнусть в теории должна быть). Ветки, которые приводя к вершинам с противоречиями в формулах имеют вид (справа дана причина обрыва ветки):
 P(a),  Q(a),  P(f(a)),  Q(f(a))    ложно 3: !Q(f(a))
 P(a),  Q(a),  P(f(a)), !Q(f(a))    ложно 1: P(f(a)) ∨ !Q(f(a))
 P(a),  Q(a), !P(f(a))              ложно 2: P(f(a))
 P(a), !Q(a)                        ложно 1: !P(a) ∨ Q(a)

!P(a),  Q(a),  P(f(a)),  Q(f(a))    ложно 3: !Q(f(a))
!P(a),  Q(a),  P(f(a)), !Q(f(a))    ложно 1: P(f(a)) ∨ !Q(f(a))
!P(a),  Q(a), !P(f(a))              ложно 2: P(f(a))
!P(a), !Q(a),  P(f(a)),  Q(f(a))    ложно 3: !Q(f(a))
!P(a), !Q(a),  P(f(a)), !Q(f(a))    ложно 1: P(f(a)) ∨ !Q(f(a))
!P(a), !Q(a), !P(f(a))              ложно 2: P(f(a))

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

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


Недедуктивные выводы

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


Обзор программ машинного вывода

Стартовую информацию можно найти на wiki. Большой список существующих систем есть на github.

Существует "Thousands of Problems for Theorem Provers (TPTP) Problem Library", которая используется в соревнованиях систем машинного вывода "CADE ATP System Competition". Соревнования проходят ежегодно, в рамках конференции CASC. В последние годы победителями являются пакеты: Vampire, Satallax, Paradox, iProver, SPASS и другие. Многие пакеты активно развиваются в Германии.


SPASS

Создан группой "Automation of Logic" из "Max Planck Institute for Computer Science", Германия. Есть он-лайн версия, консольная (Linux, Windows) и простенький GUI- интерфейс.

Пример кода для задачи:
"Есть три ящика a,b,c. Известно, что in(a,c); !in(b,c). Необходимо доказать, что !in(b,a)."

begin_problem(Inside).                 % Описание задачи
list_of_descriptions.
   name({*Inside*}). author({**}). status(unsatisfiable). description({*  *}).
end_of_list.

list_of_symbols.
   functions[(a,0), (b,0), (c,0)].      % Список констант
   predicates[(in,2)].                  % Список предикатов
end_of_list.

list_of_formulae(axioms).              % Список аксиом для отношения in

   formula(forall([x],     not(in(x,x)))).
   formula(forall([x,y],   implies( in(x,y), not(in(y,x))))).
   formula(forall([x,y,z], implies( and(in(x,y),in(y,z)), in(x,z)))).
   formula(forall([x,y,z], implies( and(in(z,x),in(z,y)), or(in(x,y),in(y,x),equal(x,y))))).

   formula(    in(a,c) ).                 % Список фактов
   formula(not(in(b,c))).

end_of_list.

list_of_formulae(conjectures).         % Список доказываемых гипотез
   formula(not(in(b,a))).
end_of_list.

end_problem.

SPASS выдает последовательность вывода (на несколько птичьем языке):

2 [0:Inp]         ||  -> in(a,c)*.
1 [0:Inp]         ||  -> in(b,a)*.
4 [0:Inp]         || in(b,c)* -> .
3 [0:Inp]         || in(U,U)* -> .
10[0:Res:1.0,5.0] || in(a,b)* -> .
9 [0:Res:1.0,6.0] || in(a,U) -> in(b,U)*.
13[0:Res:1.0,6.1] || in(U,b)* -> in(U,a).
5 [0:Inp]         || in(U,V)* in(V,U)* -> .
6 [0:Inp]         || in(U,V)* in(W,U)* -> in(W,V)*.
8 [0:Res:1.0,7.0] || in(b,U)* -> in(U,a)* equal(a,U) in(a,U).
7 [0:Inp]         || in(U,V)* in(U,W)* -> equal(W,V) in(V,W)* in(W,V)*.
	Given clause: 2[0:Inp]          ||  -> in(a,c)*.
	Given clause: 1[0:Inp]          ||  -> in(b,a)*.
	Given clause: 4[0:Inp]          || in(b,c)*+ -> .
	Given clause: 10[0:Res:1.0,5.0] || in(a,b)*+ -> .
	Given clause: 3[0:Inp]          || in(U,U)*+ -> .
	Given clause: 9[0:Res:1.0,6.0]  || in(a,U)+ -> in(b,U)*.
В конце пишет Proof found (в примере выше) или Completion found, если в доказываемых гипотезах есть ложное утверждение типа in(b,a) или не выводимое утверждение типа in(a,b). Различие между этими случаями система не делает.


Otter

Otter 3.3 Theorem Prover и Mace 2.2 Finite Model Searcher активно развивался до 2003 г. Имеет более читаемый синтаксис, чем SPASS. Доступны исходники на C и консольная версия. Есть какая-то проблема с созданием своих файлов (пришлось код копировать в уже существующие файлы). Пример с ящиками выглядит следующим образом:

set(auto).

formula_list(usable).

all x             ( -in(x,x) ).
all x all y       ( in(x,y) -> -in(y,x) ).
all x all y all z ( in(x,y) & in(y,z) -> in(x,z) ).
all x all y all z ( in(z,x) & in(z,y) -> in(x,y) | in(y,x) | x=y ).

 in(a,c).                              % факты
-in(b,c).

 in(b,a).                              % отрицание доказываемого 

end_of_list.

В отличии от SPASS, то что доказывается надо сразу брать с отрицанием (выше in(b,a)) и оно не отличается списка "истинных" предложений. Если написать -in(b,a), то Otter, в отличии от SPASS, не останавливается (по крайней мере при стандартных настройках). Доказательство выглядит так:

3 [] -in(x,y)| -in(y,z) | in(x,z).    % используемая аксиома
5 [] -in(b,c).                        % факты
7 [] in(a,c).
8 [] in(b,a).
13 [hyper,8,3,7] in(b,c).             % вывод
14 [binary,13.1,5.1] $F.              % получено противоречие

Задача "Стимроллер"

Эта задача предложена Шубертом в 1978 г. При ненаправленном порождении формул она приводит к экспоненциальному росту числа формул, поэтому часто используется при тестировании систем машинного вывода.

Существуют волки, лисы, птицы, гусеницы и улитки.
Волки, лисы, птицы, гусеницы и улитки — животные.
Существуют злаки. Злаки — растения.
Животное либо ест все растения, либо всех животных, которые меньше него и едят некоторые растения.
Гусеницы и улитки меньше птиц. Птицы меньше лис. Лисы меньше волков.
Волки не едят лис и злаки. Птицы едят гусениц и не едят улиток. Гусеницы и улитки едят некоторые растения.
Cуществует животное, которое ест некоторых питающихся злаками животных (необходимо доказать).

P(x): растение; A(x): животное; B(x): птица; W(x): волк; F(x): лиса; C(x): гусеница; G(x): злак; S(x): улитка;
E(x,y): x ест y; L(x,y) : x меньше, чем y.

xW(x),  ∃xF(x),  ∃xB(x),  ∃xC(x),  ∃xS(x),  ∃xG(x),
W(x) → A(x) → A(x),  F(x) → A(x),  B(x) → A(x),  C(x) → A(x), S(x) → A(x),   
G(x) → P(x)
A(x) & A(z) & P(y) & P(v) & L(z,x) & E(z,v) → E(x,y) ∨ E(x,z)
C(x) & B(y)  →  L(x,y)
S(x) & B(y)  →  L(x,y)
B(x) & F(y)  →  L(x,y)
F(x) & W(y)  →  L(x,y)
W(x) & F(y)  → !E(x,y)
W(x) & G(y)  → !E(x,y)
B(x) & C(y)  →  E(x,y)
B(x) & S(y)  → !E(x,y)
C(x) → ∃y [P(y) & E(x,y)] 
S(x) → ∃y [P(y) & E(x,y)] 

∃x,y[A(x) & A(y) & E(x,y) & ∃z[G(z) & E(y,z)]]

В пакте Otter есть пример steam.in с этой задачей.


Литература