prolog - 有人见过 SATCHMO 定理证明器的一个很好的开源 Prolog 实现吗？

Question

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

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

Answer 1

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

Rainer Manthey and François Bry. SATCHMO: A Theorem Prover Implemented in Prolog. In Proceedings of the 9th International Conference on Automated Deduction, pages 415–434. Springer-Verlag, 1988.

本文介绍了 Satchmo 的几种 Prolog 实现并讨论了它们的优点。还给出了一些例子。这是一个 Satchmo 版本，我用它作为我的 Reasoner RACE for Attempto Controlled English 的起点:

:- 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.