क्या किसी ने SATCHMO प्रमेय समर्थक के एक अच्छा ओपन सोर्स प्रोलॉग कार्यान्वयन देखा है?

Question

मैंने प्रोटोमो प्रमेय के बारे में बात करते हुए सैचमो प्रमेय समर्थक पर कुछ कागजात देखे हैं। लेकिन अब तक एकमात्र स्रोत कोड कार्यान्वयन मैंने पाया है और यह वास्तव में सीमित था और इसका मतलब केवल उदाहरण देने के लिए किया गया था कि नियमों का मूल्यांकन कैसे किया गया था और निकाल दिया गया था। क्या किसी ने प्रोलॉग में सैचमो के अच्छे ओपन सोर्स कार्यान्वयन को देखा है?

नोट, मैं सैचमो नामक Django के लिए पाइथन भाषा उपकरण का जिक्र नहीं कर रहा हूं, यही कारण है कि मैंने टैग में सैचमो शामिल नहीं किया था, क्योंकि स्टैक ओवरफ़्लो उस टैग के लिए प्रमुख परिभाषा के रूप में दिखाता है।

Answer 1

मुझे किसी भी तरह पता था कि मुझे कुछ दिन अफसोस होगा जब मैंने एक महीने पहले बिन में अपने मास्टर थीसिस के लिए एकत्र किए गए सभी कागजात को चकित किया था। चूंकि मेरी थीसिस बाधाओं के साथ सैचमो को विस्तारित करने के बारे में थी, इसलिए विभिन्न कार्यान्वयन दिखाते हुए सैचमो पर कुछ पेपर थे ...

वैसे भी, शुरू करने के लिए एक अच्छा बिंदु यहां होगा: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich। प्रोफेसरों में से एक, फ्रैंकोइस ब्रा, सैचमो के डेवलपर्स में से एक थे, और उनकी इकाई ने विभिन्न दिशाओं में इसे विस्तारित करने के लिए काफी काम किया। संकलन सैचमो पर एक नज़र डालें। पीएमएस संस्थान के लोग स्पष्टीकरण में सक्षम होना चाहिए यदि आप गैर-शैक्षणिक कार्य के लिए कोड का उपयोग कर सकते हैं। अकादमिक काम के लिए, यह कोई समस्या नहीं होनी चाहिए।

सब बातों Satchmo पर अवलोकन के लिए (हालांकि कुछ साल पहले ही वर्ष), तो आप इस ग्रंथ सूची का उपयोग कर सकते हैं: Variations on a Theme

Answer 2

Satchmo (यह भी उपर्युक्त "एक विषय पर बदलाव" में सूचीबद्ध) पर पहले कागज

रेनर मंथी और फ्रैंकोइस ब्रा। SATCHMO: प्रोलॉग में एक प्रमेय प्रवर्तन लागू। स्वचालित कटौती पर 9वें अंतर्राष्ट्रीय सम्मेलन की कार्यवाही में, पृष्ठ 415-434। स्प्रिंगर-वेरलाग, 1 9 88.

पेपर सैचमो के कई प्रोलॉग कार्यान्वयन प्रस्तुत करता है और उनकी योग्यता पर चर्चा करता है। कुछ उदाहरण दिए गए हैं।

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