Có ai nhìn thấy một nguồn mở Prolog thực hiện tốt của định lý SATCHMO prover?

Question

Tôi đã nhìn thấy khá một vài bài báo về định lý SATCHMO prover nói về triển khai Prolog. Nhưng việc triển khai mã nguồn duy nhất mà tôi đã tìm thấy cho đến nay là trong một cuốn sách và nó thực sự bị hạn chế và chỉ có nghĩa là để đưa ra một ví dụ về cách các quy tắc được đánh giá và kích hoạt như thế nào. Có ai nhìn thấy một thực thi mã nguồn mở tốt của SATCHMO trong Prolog? Lưu ý, tôi không đề cập đến công cụ ngôn ngữ Python cho Django được gọi là Satchmo, đó là lý do tại sao tôi không bao gồm Satchmo trong các thẻ vì đó là những gì Stack Overflow hiển thị như là định nghĩa chi phối cho thẻ đó.

Answer 1

Tôi bằng cách nào đó biết rằng tôi sẽ hối tiếc một ngày nào đó khi tôi cười tất cả các giấy tờ mà tôi đã thu thập cho luận án thạc sĩ của tôi vào thùng rác một tháng trước. Vì luận án của tôi là về việc mở rộng SATCHMO với các ràng buộc, có một vài giấy tờ về SATCHMO cho thấy các triển khai khác nhau ...

Dù sao, một điểm tốt để bắt đầu sẽ ở đây: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich. Một trong những giáo sư, Francois Bry, là một trong những nhà phát triển của SATCHMO, và đơn vị của ông đã làm khá nhiều công việc để mở rộng nó theo các hướng khác nhau. Có một cái nhìn tại Compiling SATCHMO. Những người ở viện PMS nên có thể làm rõ nếu bạn có thể sử dụng mã cho công việc phi học thuật. Đối với công việc học tập, nó không phải là vấn đề.

Đối với một cái nhìn tổng quan về tất cả mọi thứ Satchmo (mặc dù một vài năm tuổi đã được), bạn có thể sử dụng thư mục này: Variations on a Theme

Answer 2

Các bài báo đầu tiên trên Satchmo (cũng được liệt kê trong "Variations trên Theme" được đề cập ở trên) là

Rainer Manthey và François Bry. SATCHMO: Một Prover Định lý được thực hiện trong Prolog. Trong Kỷ yếu Hội nghị Quốc tế lần thứ 9 về Khấu trừ Tự động, các trang 415–434. Springer-Verlag, 1988.

Bài báo trình bày một số triển khai Prolog của Satchmo và thảo luận về giá trị của chúng. Cũng được đưa ra là một số ví dụ. Dưới đây là một phiên bản Satchmo mà tôi sử dụng như là điểm bắt đầu của RACE lý luận của tôi cho Attempto kiểm soát tiếng Anh:

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