SPASS прувер, немного о нем

SPASS. Поддерживает свой формат для ввода формул. Образец (на примере Сократа)

begin_problem(Sokrates1).
list_of_descriptions.
name({*Sokrates*}).
author({*Christoph Weidenbach*}).
status(unsatisfiable).
description({* Sokrates is mortal and since all humans are mortal, he is mortal too. *}).
end_of_list.
list_of_symbols.
functions[(sokrates,0)].
predicates[(Human,1),(Mortal,1)].
end_of_list.
list_of_formulae(axioms).
formula(Human(sokrates),1).
formula(forall([x],implies(Human(x),Mortal(x))),2).
end_of_list.
list_of_formulae(conjectures).
formula(Mortal(sokrates),3).
end_of_list.
end_problem.

То бишь, три части. Описательная часть; часть, где указаны сигнатуры, часть, где даны все аксиомы, и наконец – часть, где указано то, что надо доказывать.
Пример вывода для данной задачи.

Input Problem:

1[0:Inp] ||  -> Human(sokrates)*.

2[0:Inp] || Mortal(sokrates)* -> .

3[0:Inp] || Human(U) -> Mortal(U)*.

 This is a monadic Horn problem without equality.

 This is a problem that has, if any, a finite domain model.

 There are no function symbols.

 This is a problem that contains sort information.

 The conjecture is ground.

 The following monadic predicates have finite extensions: Human.

 Axiom clauses: 2 Conjecture clauses: 1

 Inferences: IEmS ISoR IORe 

 Reductions: RFClR RBClR RObv RUnC RTaut RSST RSSi RFSub RBSub RCon 

 Extras    : Input Saturation, Always Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1

 Precedence: Mortal > Human > sokrates

 Ordering  : KBO

Processed Problem:

Worked Off Clauses:

Usable Clauses:

1[0:Inp] ||  -> Human(sokrates)*.

2[0:Inp] || Mortal(sokrates)* -> .

3[0:Inp]Human(U) ||  -> Mortal(U)*.

SPASS V 1.0.0

SPASS beiseite: Proof found.

Problem: sokrates1.dfg 

SPASS derived 1 clauses, backtracked 0 clauses and kept 4 clauses.

SPASS allocated 438 KBytes.

SPASS spent     0:00:00.12 on the problem.

                0:00:00.02 for the input.

                0:00:00.02 for the FLOTTER CNF translation.

                0:00:00.00 for inferences.

                0:00:00.00 for the backtracking.

                0:00:00.00 for the reduction.

--------------------------SPASS-STOP------------------------------

SPASS читает формулу и приводит ее к КНФ, где отрицание conjecture, т.к SPASS основан на опровержении. Клозы

1[0:Inp] ||  -> Human(sokrates)*.

2[0:Inp] || Mortal(sokrates)* -> .

3[0:Inp] || Human(U) -> Mortal(U)*.

Это наши входные клозы, где переменные при -> обозначают импликацию, * - означает, что литерал максимален (?), а отрицательные литералы слева от || являются monadic литералами с переменным аргументом, который обрабатывается SPASS. Далее SPASS анализирует задачу и обнаруживает, что

This is a monadic Horn problem without equality.

This is a problem that has, if any, a finite domain model.

There are no function symbols.

This is a problem that contains sort information.

The conjecture is ground.

The following monadic predicates have finite extensions: Human.

Axiom clauses: 2 Conjecture clauses: 1

Основываясь на этой информации SPASS принимает следующие настройки:

Inferences: IEmS ISoR IORe 

Reductions: RFClR RBClR RObv RUnC RTaut RSST RSSi RFSub RBSub RCon 

Extras    : Input Saturation, Always Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1

Precedence: Mortal > Human > sokrates

Ordering  : KBO

Включаем inference rules empty sort (IEmS) и (ISoR) и ordered resolution (IORe). Редукции forward и backward clause reduction (RFClR RBClR), obvious reductions (RObv), unit conflict (RUnC), syntactic tautology deletion (RTaut), static soft typing (RSST), sort simplification (RSSi), forward и backward subsumption (RFSub RBSub) и condensation (RCon). SPASS выбирает порядок Кнута-Бендикса (KBO), со следующим порядком Mortal > Human > sokrates.
Для такого просто примера SPASS уже нашел доказательство, но ничего не вывел.

Usable Clauses:

1[0:Inp] ||  -> Human(sokrates)*.

2[0:Inp] || Mortal(sokrates)* -> .

3[0:Inp]Human(U) ||  -> Mortal(U)*.

SPASS V 1.0.0

SPASS beiseite: Proof found.

Problem: sokrates1.dfg 

SPASS derived 1 clauses, backtracked 0 clauses and kept 4 clauses.

SPASS allocated 438 KBytes.

SPASS spent     0:00:00.12 on the problem.

                0:00:00.02 for the input.

                0:00:00.02 for the FLOTTER CNF translation.

                0:00:00.00 for inferences.

                0:00:00.00 for the backtracking.

                0:00:00.00 for the reduction.

По дефолту он ничего и не выводит, для того, чтобы SPASS выводил доказательство введите опцию -DocProof.

Here is a proof with depth 1, length 5 :

1[0:Inp] ||  -> Human(sokrates)*.

2[0:Inp] || Mortal(sokrates)* -> .

3[0:Inp]Human(U) ||  -> Mortal(U)*.

4[0:Res:3.1,2.0]Human(sokrates) ||  -> .

5[0:ClR:4.0,1.0] ||  -> .

Formulae used in the proof : 1 3 2