anldp - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

anldp - डेविस-पुटनम प्रस्तावात्मक संतुष्टि प्रक्रिया का कार्यान्वयन

SYNOPSIS

एनएलडीपी [विकल्पों] इनपुट फ़ाइल > निर्गम संचिका

वर्णन

यह मैनुअल पेज संक्षेप में दस्तावेज करता है एनएलडीपी आदेश।

एनएलडीपी प्रस्ताव के लिए डेविस-पुटनम प्रक्रिया का कार्यान्वयन है
संतुष्टि की समस्या. एनएलडीपी द्वारा प्रयुक्त प्रक्रिया को उजागर करता है गदा2(1) निर्धारित करना
संतुष्टि एनएलडीपी समानता और ए के साथ प्रथम-क्रम तर्क में भी बयान ले सकते हैं
डोमेन का आकार n फिर आकार के मॉडल खोजें n. प्रथम-क्रम मॉडल-खोज कोड
कथनों को प्रस्तावात्मक खंडों के सेट में बदल देता है जैसे कि प्रथम-क्रम
कथनों में आकार का एक मॉडल होता है n यदि और केवल यदि प्रस्तावात्मक खंड हैं
संतोषजनक. फिर प्रस्तावित सेट डेविस-पुटनम कोड को दिया जाता है; कोई
प्रस्तावित मॉडल जो पाए जाते हैं उन्हें प्रथम-क्रम के मॉडल में अनुवादित किया जा सकता है
बयान. प्रथम-क्रम मॉडल-खोज कार्यक्रम केवल सपाट रूप में कथन स्वीकार करता है
फ़ंक्शन प्रतीकों के बिना संबंधपरक खंड प्रपत्र।

विकल्प

-s उपसंग्रहण करें. (सब्समिशन हमेशा यूनिट प्रीप्रोसेसिंग के दौरान किया जाता है।)

-p मॉडल मिलते ही प्रिंट करें।

-m n रुकें जब nवां मॉडल मिल गया है.

-t n बाद में रुकें n सेकंड.

-k n अधिक से अधिक आवंटन करें n खंडों के भंडारण के लिए kbytes.

-x n क्वासिग्रुप प्रयोग n.

-B पट्टिका
किसी फ़ाइल में असाइनमेंट का बैकअप लें।

-b n बैकअप असाइनमेंट हर n सेकंड.

-R पट्टिका
किसी फ़ाइल से असाइनमेंट पुनर्स्थापित करें। फ़ाइल में आमतौर पर केवल अंतिम पंक्ति होती है
एक बैकअप फ़ाइल. अन्य इनपुट, विशेष रूप से खंड, बिल्कुल वैसे ही दिए जाने चाहिए
मूल खोज.

-n n इस विकल्प का उपयोग प्रथम-क्रम मॉडल खोजों के लिए किया जाता है। पैरामीटर n निर्दिष्ट करता है
डोमेन का आकार, और इसकी उपस्थिति प्रोग्राम को प्रथम-क्रम को फ़्लैट पढ़ने के लिए कहती है
प्रस्तावात्मक उपवाक्यों के बजाय संबंधपरक इनपुट उपवाक्य।

onworks.net सेवाओं का उपयोग करके ऑनलाइन anldp का उपयोग करें