有没有人看过SATCHMO定理证明器的一个很好的开源Prolog实现？

Question

我在SATCHMO定理证明器上看过很多关于Prolog实现的论文.但到目前为止我发现的唯一源代码实现是在一本书中,它实际上是有限的,仅仅是为了给出一个如何评估和解雇规则的例子.有没有人在Prolog中看到过SATCHMO的开源实现？

注意,我不是指Django的Python语言工具Satchmo,这就是为什么我没有在标签中包含Satchmo,因为这就是Stack Overflow显示为该标签的主要定义.

Answer 1

关于Satchmo的第一篇论文(也在上面提到的"主题变奏曲"中列出)是

Rainer Manthey和FrançoisBry.SATCHMO:在Prolog中实现了一个定理证明.在第9届国际自动演绎会议论文集,第415-434页.Springer-Verlag,1988.

本文介绍了Satchmo的几个Prolog实现,并讨论了它们的优点.还给出了一些例子.这是一个Satchmo版本,我用作Attempto Controlled English的推理者RACE的起点:

:- op(1200, xfx, '--->').
:- unknown(_, fail).

satisfiable :-
  setof(Clause, violated_instance(Clause), Clauses),
  !,
  satisfy_all(Clauses),
  satisfiable.
satisfiable.

violated_instance((B ---> H)) :-
  (B ---> H),
  B,
  \+ H.

satisfy_all([]).

satisfy_all([(_B ---> H) | RestClauses]) :-
  H,
  !,
  satisfy_all(RestClauses).
satisfy_all([(_B ---> H) | RestClauses]) :-
  satisfy(H),
  satisfy_all(RestClauses).

/*
satisfy((A,B)) :-
  !,
  satisfy(A),
  satisfy(B).  
*/

satisfy((A;B)) :-
  !,
  (satisfy(A) ; satisfy(B)).  

satisfy(Atom) :-
  \+ Atom = untrue,
  (
    predicate_property(Atom, built_in)
    ->
    call(Atom)
  ;
    assume(Atom)
  ).

assume(Atom) :-
%  nl, write(['Asserting  ': Atom]),
  asserta(Atom).

assume(Atom) :-
%  nl, write(['Retracting ': Atom]),
  retract(Atom),
  !,
  fail.         

Answer 2

当我把一个月前收集的所有硕士论文论文扔进垃圾箱时，我不知何故知道有一天我会后悔的。由于我的论文是关于在约束条件下扩展 SATCHMO，因此有几篇关于 SATCHMO 的论文展示了不同的实现......

\n\n

不管怎样，这里是一个很好的起点：Software Collection of the Lehr- und Forschungseinheit f\xc3\xbcr Programmier- und Modellierungssprachen, LMU 慕尼黑。其中一位教授 Francois Bry 是 SATCHMO 的开发者之一，他的部门在向不同方向扩展 SATCHMO 方面做了大量工作。看一下编译 SATCHMO。PMS 研究所的人员应该能够澄清您是否可以使用该代码进行非学术工作。对于学术工作来说，应该没有问题。

\n\n

要了解 SATCHMO 的所有内容（尽管已经有几年历史了），您可以使用以下参考书目：主题变奏

\n