एल्गोरिदम

Question

के लिए सबूत लिखना हाय दोस्तों मैं 2 एल्गोरिदम की तुलना करने की कोशिश कर रहा हूं और सोचा कि मैं उनके लिए सबूत लिख सकता हूं और लिख सकता हूं !!! (मेरी गणित तो इसलिए प्रश्न बेकार)

आम तौर पर हमारे गणित सबक पिछले वर्ष में

हम

की तरह एक प्रश्न दी जाएगी साबित: (2R + 3) = n (एन + 4)

तो मैं आवश्यक 4 चरणों को करूंगा और अंत में उत्तर प्राप्त करूंगा

जहां मैं अटक गया हूं प्राइम और क्रस्कल साबित कर रहा हूं - मैं इन एल्गोरिदम को ऊपर गणित के रूप में कैसे बना सकता हूं ताकि मैं

साबित कर सकूं

नोट: मैं लोगों से जवाब देने के लिए नहीं कह रहा हूं मेरे लिए यह wer - बस मेरी मदद एक रूप में इसे पाने मैं हो सकता है जहां एक अपने आप को जाना

धन्यवाद

Answer 1

आप कई विवरण देना नहीं है लेकिन वहाँ के गणितज्ञों का एक समुदाय है (गणितीय ज्ञान प्रबंधन MKM) जिन्होंने गणित के कंप्यूटर प्रमाणों का समर्थन करने के लिए उपकरण विकसित किए हैं। उदाहरण के लिए देखें,:

http://imps.mcmaster.ca/

और विश्वविद्यालय मैं (अस्पष्ट) पर नवीनतम सम्मेलन

http://www.orcca.on.ca/conferences/cicm09/mkm09/

Answer 2

मेरी गणित की कक्षाओं से prims साबित याद है और Kruskals एल्गोरिदम - और आप पर हमला न करें इसे गणितीय रूप में लिखकर। इसके बजाय, आप ग्राफ के लिए सिद्ध सिद्धांत लेते हैं और उन्हें गठबंधन करते हैं उदा। सबूत बनाने के लिए http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness।

यदि आप जटिलता साबित करना चाहते हैं, तो बस एल्गोरिदम के काम से यह ओ (एन^2) है। विशेष मामले के लिए कुछ अनुकूलन हैं जहां ग्राफ स्पैस है जो इसे ओ (nlogn) में कम कर सकता है।

Answer 3

कहाँ मैं अटक कर रहा हूँ prims और Kruskals साबित हो रहा है - मैं कैसे साबित करने के लिए

मुझे नहीं लगता कि आप कर सकते हैं तो मैं आगे बढ़ सकते हैं ऊपर mathmatical एक की तरह एक फार्म करने के लिए इन एल्गोरिदम प्राप्त कर सकते हैं सीधे। इसके बजाए, साबित करें कि दोनों एमएसटी उत्पन्न करते हैं, फिर साबित करें कि कोई भी दो एमएसटी बराबर है (या समतुल्य है, क्योंकि आपके पास कुछ ग्राफों के लिए एक से अधिक एमएसटी हो सकते हैं)। यदि दोनों एल्गोरिदम एमएसटी उत्पन्न करते हैं जो बराबर दिखाए जाते हैं, तो एल्गोरिदम बराबर होते हैं।

Answer 4

एल्गोरिदम की शुद्धता साबित करने के लिए, आपको आम तौर पर (ए) दिखाना होता है कि यह समाप्त हो जाता है और (बी) कि इसका आउटपुट आप जो करने की कोशिश कर रहे हैं उसके विनिर्देश को पूरा करता है। ये दो सबूत आपके प्रश्न में उल्लिखित बीजगणितीय सबूत से अलग होंगे। आपको जिस महत्वपूर्ण अवधारणा की आवश्यकता है वह mathematical induction है। (यह सबूत के लिए recursion है।)

चलिए quicksort उदाहरण के रूप में लें।

साबित करने के लिए कि quicksort हमेशा समाप्त हो जाता है, तो आपको पहले पता चलेगा कि यह लंबाई 1. के इनपुट के लिए समाप्त हो जाता है (यह तुच्छता से सच है।) इसके बाद पता चलता है कि अगर यह करने के लिए n लंबाई के इनपुट के लिए समाप्त हो जाता है, तो यह होगा लंबाई एन + 1 के इनपुट के लिए समाप्त करें। प्रेरण के लिए धन्यवाद, यह साबित करने के लिए पर्याप्त है कि एल्गोरिदम सभी इनपुट के लिए समाप्त हो जाता है।

साबित करने के लिए कि quicksort सही है, तो आपको सटीक गणितीय भाषा के लिए छँटाई तुलना के विनिर्देश परिवर्तित करना होगा। हम उत्पादन इनपुट इस तरह के एक permutation होना चाहता हूँ कि अगर मैं ≤ जे तो एक _मैं ≤ एक _जे। यह साबित करना कि Quicksort का आउटपुट इनपुट का क्रमपरिवर्तन आसान है, क्योंकि यह इनपुट के साथ शुरू होता है और केवल तत्वों को स्वैप करता है। दूसरी संपत्ति प्रदान करना थोड़ा सा ट्रिकियर है, लेकिन फिर आप प्रेरण का उपयोग कर सकते हैं।

Answer 5

अधिकांश समय सबूत समस्या आप अपने हाथ में पर निर्भर करता है। सरल तर्क समय पर पर्याप्त जा सकता है, कुछ अन्य समय में आप कठोर सबूत आवश्यकता हो सकती है। मैंने एक बार अपने एल्गोरिदम को सही ठहराने के लिए पहले से साबित प्रमेय का एक अनुशासनिक और सबूत इस्तेमाल किया था। लेकिन यह एक कॉलेज परियोजना के लिए है।

Answer 6

शायद तुम एक अर्द्ध स्वचालित सबूत विधि की कोशिश करना चाहते हैं। बस कुछ अलग करने के लिए;) उदाहरण के लिए, यदि आपके पास प्राइम और क्रस्कल के एल्गोरिदम का जावा विनिर्देश है, तो उसी ग्राफ मॉडल पर बेहतरीन रूप से निर्माण करना, आप KeY Prover का उपयोग एल्गोरिदम के समतुल्य साबित करने के लिए कर सकते हैं।

महत्वपूर्ण हिस्सा गतिशील तर्क में अपने प्रमाण दायित्व (इस प्रकार के और जावा कार्यक्रमों का प्रतीक निष्पादन के साधन के साथ पहले क्रम तर्क का एक विस्तार है) को औपचारिक रूप देने है।

\forall Graph g. \exists Tree t. 
    (<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t) 

यह व्यक्त करता है कि सभी रेखांकन के लिए, दोनों एल्गोरिदम समाप्त कर देंगे और परिणाम एक ही पेड़ है: सूत्र साबित करने के लिए निम्नलिखित (अधूरा) पैटर्न से मेल खा सकते।

आप भाग्यशाली हैं और अपने सूत्र (और एल्गोरिथ्म कार्यान्वयन) सही हैं, तो कुंजी यह स्वचालित रूप से आप के लिए साबित कर सकते हैं। यदि नहीं, तो आपको कुछ मात्रात्मक चर को तुरंत चालू करने की आवश्यकता हो सकती है जो पिछले प्रमाण पेड़ का निरीक्षण करने के लिए आवश्यक बनाता है।

केवाई के साथ बात साबित करने के बाद, आप या तो कुछ सीखने के बारे में खुश रह सकते हैं या केवाई सबूत से मैनुअल सबूत का पुनर्निर्माण करने का प्रयास कर सकते हैं - यह एक कठिन काम हो सकता है क्योंकि केवाई जावा के लिए बहुत से नियमों को जानता है जो कि समझना आसान नहीं है। हालांकि, हो सकता है कि आप कुछ ऐसे शब्दों से एक हेब्रैंड विच्छेदन निकालने की तरह कुछ कर सकें जो कि केवाई प्रूफ में अनुक्रमों के दाईं ओर मौजूद अस्तित्व वाले क्वांटिफायर को तुरंत चालू करता था।

ठीक है, मुझे लगता है कि कुंजी एक दिलचस्प उपकरण है और अधिक लोगों को इस तरह उपकरण का उपयोग कर महत्वपूर्ण जावा कोड साबित करने के लिए इस्तेमाल किया जाना चाहिए;)