Qualcuno ha visto una buona implementazione Prolog open source del dimostratore di teoremi SATCHMO?

Question

Ho visto parecchi articoli sul dimostratore del teorema SATCHMO che parlano di implementazioni Prolog. Ma l'unica implementazione del codice sorgente che ho trovato finora era in un libro ed era davvero limitata e voleva solo dare un esempio di come le regole venivano valutate e licenziate. Qualcuno ha visto una buona implementazione open source di SATCHMO in Prolog?

Nota, non mi riferisco allo strumento di linguaggio Python per Django chiamato Satchmo, che è il motivo per cui non ho incluso Satchmo nei tag poiché è quello che Stack Overflow mostra come definizione dominante per quel tag.

Answer 1

In qualche modo sapevo che un giorno mi sarei pentito di aver buttato tutti i documenti che avevo raccolto per la mia tesi di laurea nel cestino un mese fa. Poiché la mia tesi riguardava l'estensione del SATCHMO con restrizioni, c'erano alcuni documenti su SATCHMO che mostravano diverse implementazioni ...

In ogni caso, un buon punto di partenza sarebbe qui: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich. Uno dei professori, Francois Bry, era uno degli sviluppatori di SATCHMO, e la sua unità ha fatto un bel po 'di lavoro per estenderlo in diverse direzioni. Dai un'occhiata alla Compilazione SATCHMO. Le persone dell'istituto PMS dovrebbero essere in grado di chiarire se è possibile utilizzare il codice per il lavoro non accademico. Per il lavoro accademico, non dovrebbe essere un problema.

Per una panoramica su tutte le cose Satchmo (anche se un paio di anni già), è possibile utilizzare questa bibliografia: Variations on a Theme

Answer 2

Il primo documento su Satchmo (anche elencati nella sezione "Variazioni su un tema" di cui sopra) è

Rainer Manthey e François Bry. SATCHMO: Un teorico di proverbi implementato in Prolog. In Atti del 9 ° Convegno internazionale sulla deduzione automatizzata, pagine 415-434. Springer-Verlag, 1988.

Il documento presenta numerose implementazioni Prolog di Satchmo e ne discute i meriti. Anche dato sono alcuni esempi. Ecco una versione Satchmo che ho usato come punto di partenza della mia ragionatore RACE per Attempto controllata inglese:

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