Has anybody seen a good open source Prolog implementation of the SATCHMO theorem prover?
-
27-04-2021 - |
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.
Solution
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
OTHER TIPS
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.