यह कमांड मैस4 है जिसे हमारे कई मुफ्त ऑनलाइन वर्कस्टेशन जैसे उबंटू ऑनलाइन, फेडोरा ऑनलाइन, विंडोज ऑनलाइन एमुलेटर या मैक ओएस ऑनलाइन एमुलेटर में से एक का उपयोग करके ऑनवर्क्स फ्री होस्टिंग प्रदाता में चलाया जा सकता है।
कार्यक्रम:
नाम
mace4 - पहले क्रम के बयानों के परिमित प्रतिरूपों की खोज करता है
SYNOPSIS
गदा4 [विकल्पों] इनपुट फ़ाइल > निर्गम संचिका
वर्णन
यह मैनुअल पेज संक्षेप में दस्तावेज करता है गदा4 आदेश।
कार्यक्रम गदा4 प्रथम-क्रम और समीकरण को संतुष्ट करने वाली परिमित संरचनाओं की खोज करता है
बयान, उसी तरह का बयान कि कहावत9(1) स्वीकार करता है। यदि कथन है
कुछ अनुमानों का खंडन, किसी भी संरचना द्वारा पाया गया गदा4 के प्रति उदाहरण हैं
अनुमान। गदा4 के लिए एक मूल्यवान पूरक हो सकता है कहावत9(1) प्रति-उदाहरणों की तलाश में
उपयोग करने से पहले (या उसी समय) कहावत9(1) सबूत खोजने के लिए। यह भी हो सकता है
डिबग इनपुट क्लॉज और फ़ार्मुलों के लिए उपयोग किया जाता है कहावत9(1).
विकल्प
विकल्पों का सारांश नीचे दिया गया है। विकल्प में दी गई समकक्ष सेटिंग्स को ओवरराइड करते हैं
इनपुट फ़ाइल। ध्वज को सेट या साफ़ करने के लिए, आपको मान के रूप में 1 या 0 देना होगा।
-मदद इससे पता गदा4 इन कमांड-लाइन विकल्पों का सारांश प्रिंट करने के लिए।
-n n यह खोज के लिए प्रारंभिक डोमेन आकार देता है। डिफ़ॉल्ट मान 2 है। यदि आप
एक भी दो -N विकल्प, गदा4 के माध्यम से डोमेन आकार को पुनरावृत्त करेगा -N मूल्य,
द्वारा दी गई वेतन वृद्धि का उपयोग करना -I मूल्य। अन्यथा, गदा4 केवल के लिए खोज करेंगे
-n मूल्य.
-N n यह खोज के लिए अंतिम डोमेन आकार देता है। डिफ़ॉल्ट 10 है।
-i n यह खोज के लिए डोमेन आकार में वृद्धि देता है। डिफ़ॉल्ट 1 है।
-q n यह ध्वज पैरामीटर पुनरावृति को ओवरराइड करता है। यह उन आकारों को आज़माने के लिए कहता है जो अभाज्य हैं
संख्या, से -n के माध्यम से -N.
-m n खोजना बंद करें जब nवें संरचना मिली है। डिफ़ॉल्ट 1 है।
-t n बाद में खोजना बंद करें n सेकंड.
-s n ज्यादा से ज्यादा अनुमति दें n प्रत्येक डोमेन आकार के लिए सेकंड। पैरामीटर का उपयोग किया जा सकता है (एक साथ
साथ में -t) एक समग्र समय सीमा देने के लिए।
-b n खोजना बंद करें जब (लगभग) n मेगाबाइट मेमोरी का उपयोग किया गया है।
-V n क्लॉज और में स्थिरांक से चर को अलग करने के लिए एक नियम की आवश्यकता है
मुक्त चर के साथ सूत्र। यदि यह ध्वज स्पष्ट है, तो चर (निचला .) से शुरू होते हैं
केस) `यू' से `जेड' तक। यदि यह ध्वज सेट है, तो खंडों में चर (ऊपरी .) से शुरू होते हैं
मामला) `ए' से `जेड' या `_'।
-P n यदि यह ध्वज सेट किया जाता है, तो पाए जाने वाले सभी ढांचे 'मानक' रूप में मुद्रित होते हैं,
जिसका अर्थ है कि वे अन्य एलएडीआर कार्यक्रमों जैसे इनपुट के रूप में उपयुक्त हैं आइसोफिल्टर(1)
और इंटरफॉर्मेट(1).
-p n यदि यह ध्वज सेट है, और यदि -P स्पष्ट है, सभी संरचनाएं जो पाई जाती हैं वे मुद्रित हैं
सारणीबद्ध रूप में।
-R n यदि यह ध्वज सेट है, तो खोज के लिए एक रिंग संरचना लागू की जाती है। संचालन
{+,-,*} को पूर्णांकों का वलय माना जाता है (mod domain_size)। यह विधि डालता है
खोज पर एक सख्त बाधा, बहुत बड़ी संरचनाओं की अनुमति देता है
की जाँच की।
-v n यदि यह ध्वज सेट है, तो आउटपुट फ़ाइल खोज के बारे में जानकारी प्राप्त करती है,
प्रारंभिक आंशिक मॉडल सहित (मॉडल का वह भाग जिसे निर्धारित किया जा सकता है
बैकट्रैकिंग शुरू होने से पहले) और प्रत्येक डोमेन आकार के लिए समय और अन्य आंकड़े।
(यह बैकट्रैकिंग का कोई निशान नहीं देता है, इसलिए यह बहुत अधिक फ़ाइल का उपभोग नहीं करता है
स्थान।)
-T n यदि ट्रेस ध्वज सेट है, तो ट्रेस सहित खोज के बारे में विस्तृत जानकारी
सभी असाइनमेंट और बैकट्रैकिंग का, मानक आउटपुट पर प्रिंट किया जाता है। यह झंडा
बहुत सारे आउटपुट का कारण बनता है, इसलिए इसे केवल छोटी खोजों पर ही इस्तेमाल किया जाना चाहिए।
कई उन्नत विकल्प भी मौजूद हैं, जिनका प्रयोग प्रयोग के लिए किया जाता है
खोज के तरीके। उन्हें लगभग सभी उपयोगकर्ताओं द्वारा अनदेखा किया जा सकता है। इनके विवरण के लिए
विकल्प, मूल देखें गदा4 मैनुअल।
onworks.net सेवाओं का उपयोग करके mace4 का ऑनलाइन उपयोग करें
