¿Alguien ha visto una buena implementación de código abierto Prolog del demostrador de teoremas SATCHMO?

Question

He visto bastantes artículos en el probador de teoremas de SATCHMO que hablan sobre las implementaciones de Prolog. Pero la única implementación del código fuente que he encontrado hasta ahora estaba en un libro y era muy limitada y solo quería dar un ejemplo de cómo se evaluaban y disparaban las reglas. ¿Alguien ha visto una buena implementación de código abierto de SATCHMO en Prolog?

Nota, no me estoy refiriendo a la herramienta de lenguaje Python para Django llamada Satchmo, por eso no incluí Satchmo en las etiquetas ya que es lo que Stack Overflow muestra como la definición dominante para esa etiqueta.

Answer 1

De alguna manera sabía que me arrepentiría algún día cuando arrojara todos los papeles que había recogido para mi tesis de maestría en la papelera hace un mes. Dado que mi tesis trataba de extender SATCHMO con restricciones, había unos pocos documentos en SATCHMO que mostraban diferentes implementaciones ...

De todos modos, un buen punto para comenzar sería aquí: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich. Uno de los profesores, Francois Bry, fue uno de los desarrolladores de SATCHMO, y su unidad hizo un gran trabajo para ampliarlo en diferentes direcciones. Echa un vistazo a Compilar SATCHMO. Las personas en el instituto PMS deberían poder aclarar si puede usar el código para el trabajo no académico. Para el trabajo académico, no debería ser un problema.

Para una visión general sobre todas las cosas Satchmo (aunque unos pocos años ya), puede utilizar esta bibliografía: Variations on a Theme

Answer 2

El primer documento sobre Satchmo (también figura en las "Variaciones sobre un tema" anteriormente citado) es

Rainer Manthey y François Bry. SATCHMO: un teorema Prover implementado en Prolog. En las Actas de la 9na Conferencia Internacional sobre Deducción Automatizada, páginas 415-434. Springer-Verlag, 1988.

El artículo presenta varias implementaciones Prolog de Satchmo y analiza sus ventajas. También se dan algunos ejemplos. He aquí una versión Satchmo que he utilizado como punto de inicio de mi raza razonador de Inglés Attempto controlada:

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