SATCHMO 정리 프로 버의 Prolog 구현에 대한 좋은 오픈 소스를 본 사람이 있습니까?

Question

나는 SATCHMO 정리 프로 버에서 Prolog 구현에 대해 언급 한 논문을 꽤 많이 보았다. 그러나 지금까지 발견 한 유일한 소스 코드 구현은 책에 포함되어 있으며 실제로 제한되어 있으며 규칙이 어떻게 평가되고 해고되었는지 예제를 제공하기위한 것입니다. Prolog에서 SATCHMO의 좋은 오픈 소스 구현을 본 사람이 있습니까?

참고로 Satchmo라는 Django 용 Python 언어 도구를 언급하지 않았습니다. 그 이유는 태그에 Satchmo가 포함되지 않았기 때문입니다. 스택 오버플로가 태그의 주요 정의로 표시되는 이유이기 때문입니다.

Answer 1

나는 언젠가 내가 한 달 전에 석사 학위 논문을 위해 수집 한 모든 논문을 뽑아서 언젠가는 후회할 것임을 알았다. 저의 논문은 제약으로 SATCHMO를 확장하는 것에 관한 것이기 때문에 SATCHMO에 여러 가지 구현을 보여주는 몇 가지 논문이있었습니다 ...

어쨌든, 좋은 점은 Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich 일 것입니다. 교수 중 한 명인 Francois Bry는 SATCHMO의 개발자 중 한 명이었으며 그의 부대는 SATCHMO를 다른 방향으로 확장하는 데 많은 노력을 기울였습니다. SATCHMO 컴파일을보십시오. PMS 기관의 사람들은 학업 이외의 업무에 대한 코드를 사용할 수 있는지 여부를 명확히 할 수 있어야합니다. 학업을 위해서는 문제가되지 않아야합니다. 모든 것을 츠모 (Satchmo)에 대한 개요를

(이미 몇 살 있지만),이 참고 문헌을 사용할 수 있습니다 Variations on a Theme

Answer 2

츠모 (Satchmo) (또한 위에서 언급 한 "주제에 의한 변주곡"에 나열된)의 첫 번째 논문

Rainer Manthey와 François Bry입니다. SATCHMO : 프롤로그에서 구현 된 정리 검증기. 제 9 회 자동 공제에 관한 국제 회의록, 415-434 페이지. Springer-Verlag, 1988.

이 논문은 Satchmo의 몇 가지 Prolog 구현을 제시하고 그 장점을 설명합니다. 또한 몇 가지 예가 있습니다.

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