Beckert＆Posegga算法的Prolog实现

如何解决Beckert＆Posegga算法的Prolog实现

贝克特和波塞加通常被认为是 最短的一阶逻辑证明者。但是那里 是一个陷阱，即它需要一个准备步骤， 公式必须先以特殊形式显示 证明者可以尝试。

所以最终证明者将不仅是史诗般的 从这里几行：

https://formal.iti.kit.edu/beckert/pub/LeanTAP.pdf

我尝试在Prolog中翻译Beckert＆Posegga的算法，但是直到现在我还没有成功。可惜的是它是一种高效的算法，Prolog的翻译很有趣。

最好是希望看到75 Problems for Testing Automatic Theorem Provers正在运行的单例和完整测试用例。

解决方法

我的笔记。甚至没有执行一次！

% Only for (classical logic) closed first-order formula in:
% Skolemized Negation Normal Form (which is set up by a preprocessor)
% "Closed" means "No free variables".
%
% Negation Normal Form: https://en.wikipedia.org/wiki/Negation_normal_form
%
% 1) The negation operator is only applied to propositional variables or literals.
% 2) Only operator AND and OR are allowed.
%
% Skolemized: https://en.wikipedia.org/wiki/Skolem_normal_form 
%
% 1) In Prenex normal form
% 2) With only universal first-order quantifiers
%
% i.e. the X in exists(X) have been replaced by skolem constants
%
% This is called
%
% prove(+Fml,UnExp,Lits,FreeV,VarLim)
% 
% but is actually
%
% disprove(+Fml,VarLim)
% 
% Because the query *succeeeds* if there is a closed tableau for the 
% first-order formula bound to Fml (i.e. the formula is unsatisfiable;
% one thus passes the negation of the formula to prove to disprove/5
% (the paper uses the adjective "inconsistent" instead of "unsatisfiable"
% but "inconsistency" is a system attribute,not a formula attribute)
%
% Method of analytical tableaux: 
% https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
%
% Current branch:
%   Fml   : Formula being expanded
%   UnExp : List of formulae not yet expanded
%   Lits  : List of literals present on the current branch
%   FreeV : List of free variables on the branch (Prolog variables,possibly
%           bound to a term)
% VarLim : Upper bound for FreeV,used to initiate backtracking
%          The disprover stops its search if it has VarLim free variables on a
%          branch,and starts to backtrack. 
%
% Start with 
%
% disprove(Fml,[],VarLim)
%
% Succeed if Fml can be proven unsatisfiable without using more than VarLim
% free variables on each branch (path from root node to leaf),failure otherwise
% (i.e. either satisfiable or not enough resources -- can that be disentangled??)

% ---
% ***
% Needs a predicate which rewrites a formula into "Negation Normal Form"
% which is given in the second half of the paper,and which is a bit 
% larger than the prover itself.
% ***
% ---

% ---
% Alpha-Formula (the name for a conjunction as per Smullyan)
% Possible changes: Use a compound and/N for a conjunction of N subformulae
% ---

disprove((F1,F2),VarLim) :- 
  !,disprove(F1,[F2|UnExp],VarLim).

% ---
% Beta-Formula (the name for a disjunction as per Smullyan)
% Possible changes: Use a compound or/N for a disjunction of N subformulae
% ---

disprove((F1;F2),VarLim),disprove(F2,VarLim).

% ---
% Gamma-Formula (the name for an universally quantified formula)
% --- 

disprove(all(X,F),VarLim) :-
  !,\+length(FreeV,% limit not reached,otherwise
                                               % fail,& backtrack over the 
                                               % two last clauses
  copy_term([X,F,FreeV],[X1,F1,FreeV]),% create fresh variables for
                                               % all(X,F) but keep already seen
                                               % variables unique
  append(UnExp,[all(X,F)],UnExp1),% append all(H,I) to UnExp
  disprove(F1,UnExp1,[X1|FreeV],VarLim).  % X1 is a new free variable on
                                               % this branch

% ---
% Closing a branch if the formula turns out to be a Literal
% i.e. determining that the branch cannot be satisfied because both a 
% Formula and its Negation appear on it. A "branch" is really a set
% of formulae,the size of which increases with the depth.
% (This code feels a bit inefficient).
% ---

disprove(Lit,_,[L|Lits],_) :-
   (Lit = -Neg; -Lit = Neg) 
   -> (unify_with_occurs_check(Neg,L) ; disprove(Lit,_)).

% ---
% Closing the branch failed.
% Add the current formula (a literal) to the list of literals on the branch
% and pick a formula waiting for expansion.
% ---

disprove(Lit,[Next|UnExp],VarLim) :-
   disprove(Next,[Lit|Lits],VarLim).

% ---
% Wrapper for iterative deepening,calling disprove with higher and
% higher depth.
% ---

inc_disprove(Fml,VarLim) :- disprove(Fml,VarLim).
inc_disprove(Fml,VarLim) :- succ(VarLim,NewVarLim),inc_disprove(Fml,NewVarLim).

,

好的，第一个版本可以运行。首先是要获得 否定范式。为了提高效率，我们替换了正数 和pos/1和neg/1包装器的否定文字：

% norm(+Form,-Norm)
norm(A,R) :- var(A),!,R = pos(A).
norm((A;B),R) :- !,norm(A,C),norm(B,D),R = or(C,D).
norm((A,B),R = and(C,D).
norm(all(A,R = all(A,C).
norm(exist(A,R = exist(A,C).
norm(-A,R = neg(A).
norm(- (A;B),norm(-A,norm(-B,D).
norm(- (A,D).
norm(- all(A,C).
norm(- exist(A,C).
norm(- -A,R).
norm(-A,R = neg(A).
norm(A,pos(A)).

下一步很简单，因为我们假设输入 公式具有不同的变量。所以我们假设 用户没有输入all(X,all(X,p(X))，而是输入 all(Y,p(X))：

% herbrand(+Norm,+List,+Integer,-Integer,-Herbrand)
herbrand(pos(A),N,pos(A)).
herbrand(neg(A),neg(A)).
herbrand(or(A,L,M,or(C,D)) :-
   herbrand(A,H,herbrand(B,D).
herbrand(and(A,and(C,D).
herbrand(all(A,C) :-
   number_codes(N,R),atom_codes(F,[0'$|R]),A =.. [F|L],H is N+1,C).
herbrand(exist(A,exist(A,C)) :-
   herbrand(B,[A|L],C).

剩下的就是抽象的证明者，使用 改为and/2和or/2。进一步我们的实现使用 一种不同的迭代加深方法，以便我们可以 更好地寻找较小的证据。

测试仍在进行中，但我们已经可以进行测试 亚里士多德三段论测试用例，例如：

case(1,aristo_conversion1,(all(A,(b(A) -: -a(A))) -: all(B,(a(B) -: -b(B))))).
case(2,aristo_conversion2,(exist(A,(b(A),a(A))) -: exist(B,(a(B),b(B))))).
case(3,aristo_conversion3,(b(A) -: a(A))),exist(B,b(B)) -: exist(C,(a(C),b(C))))).
case(4,barbara,all(B,(c(B) -: b(B))) -: all(C,(c(C) -: a(C))))).
case(5,celarent,(b(A) -: -a(A))),(c(C) -: -a(C))))).
Etc...

运行测试用例向我显示（∃C）规则的数量 应用程序。总共有21个测试用例。 他们都过去了！

?- show.
test 1 passed with 1 existential rule applications.
test 2 passed with 1 existential rule applications.
test 3 passed with 2 existential rule applications.
test 4 passed with 2 existential rule applications.
test 5 passed with 2 existential rule applications.
Etc..

为了纪念我已经用证明者fitting.pl命名了文件 梅尔文·菲廷（Melvin Fitting）1990年的英勇著作

源代码：

关于马斯洛夫公式化的马斯洛夫微积分
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-fitting-pl

Isabelle / HOL的

Aristoteles测试用例
与Beckert和Posegga运营商合作
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-aristoteles-pl

,

也可以实现 Beckert & Posegga 的算法 带有发生检查标志。我们只需替换以下内容 我们代码中的代码行：

prove(L,N) :- select(pos(A),member(neg(B),unify_with_occurs_check(A,B).

unify_with_occurs_check/2 对应于看到的 unify/2 调用 在 Beckert & Posegga 算法的屏幕截图中。什么时候我们 使用发生检查标志，我们可以用以下代码替换它：

prove(L,member(neg(A),R).

以下是一些基准测试结果，再次测试了 SWI-Prolog 和 Jekejeke Prolog 的亚里士多德测试套件。显式的 unify_with_occurs_check/2 更快：

/* Jekejeke Prolog 1.4.7 */
?- time((between(1,100,_),test,fail; true)).
% Up 1,115 ms,GC 10 ms,Threads 1,102 ms (Current 02/05/21 12:36:51)
Yes
/* SWI-Prolog 8.3.18 */
?- time((between(1,fail; true)).
% 4,758,000 inferences,0.354 CPU in 0.354 seconds (100% CPU,13438628 Lips)
true.

Prolog 标志发生_检查较慢。但是 SWI-Prolog 的开销比 Jekejeke Prolog 高得多。我得到 Jekejeke Prolog 1213/1115 = 109% 和 SWI-Prolog 571/354 = 161%：

/* Jekejeke Prolog 1.4.7 */
?- time((between(1,213 ms,GC 13 ms,197 ms (Current 02/05/21 12:36:46)
Yes
/* SWI-Prolog 8.3.18 */
?- time((between(1,571,800 inferences,0.570 CPU in 0.571 seconds (100% CPU,8021222 Lips)
true.

gist 上的开源：

关于 Herbrandisized 公式的马斯洛夫微积分
显式 unify_with_occurs_check/2 调用
file-fitting-pl

关于 Herbrandisized 公式的马斯洛夫微积分
Prolog 标志发生_check
file-fitting2-pl

测试工具
file-aritstoteles-pl

亚里士多德测试用例
file-koutsoukou-pl