Has anybody seen a good open source Prolog implementation of the SATCHMO theorem prover?

Question

I've seen quite a few papers on the SATCHMO theorem prover that talk about Prolog implementations. But the only source code implementation I've found so far was in a book and it was really limited and meant only for giving an example of how rules were evaluated and fired. Has anybody seen a good open source implementation of SATCHMO in Prolog?

Note, I am not referring to the Python language tool for Django called Satchmo, which is why I did not include Satchmo in the tags since that is what Stack Overflow shows as the dominant definition for that tag.

Answer 1

I somehow knew that I would regret it some day when I chucked all the papers that I had collected for my master thesis into the bin a month ago. Since my thesis was about extending SATCHMO with constraints, there were a few papers on SATCHMO showing different implementations...

Anyway, a good point to start would be here: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich. One of the professors, Francois Bry, was one of the developers of SATCHMO, and his unit did quite a bit of work on extending it in different directions. Have a look at the Compiling SATCHMO. The people at the PMS institute should be able to clarify if you can use the code for non-academic work. For academic work, it should be no problem.

For an overview on all things SATCHMO (although a few years old already), you can use this bibliography: Variations on a Theme

Answer 2

The first paper on Satchmo (also listed in the above mentioned "Variations on a Theme") is

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.

The paper presents several Prolog implementations of Satchmo and discusses their merits. Also given are some examples. Here is a Satchmo version that I used as the start point of my 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.