prolog - 有人看过 SATCHMO 定理证明器的开源 Prolog 实现吗？

Question

我已经看过很多关于 SATCHMO 定理证明器的论文，它们讨论了 Prolog 的实现。但是到目前为止，我发现的唯一源代码实现在一本书中，它确实很有限，仅用于举例说明如何评估和触发规则。有人在 Prolog 中看到 SATCHMO 的良好开源实现吗？

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

Answer 1

第一篇关于 Satchmo 的论文（也在上面提到的“主题变奏曲”中列出）是

Rainer Manthey 和弗朗索瓦·布赖。SATCHMO：在 Prolog 中实现的定理证明器。在第 9 届自动演绎国际会议论文集上，第 415-434 页。施普林格出版社，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 的论文展示了不同的实现......

无论如何，从这里开始是一个不错的起点：LMU Munich 的 Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen 的软件集合。其中一位教授 Francois Bry 是 SATCHMO 的开发人员之一，他的单位在将其扩展到不同方向方面做了很多工作。看看编译 SATCHMO。PMS 研究所的人员应该能够澄清您是否可以将代码用于非学术工作。对于学术工作来说，应该没问题。

有关 SATCHMO 的所有内容的概述（尽管已经有几年了），您可以使用此参考书目：主题变体