সফটওয়্যার স্ক্রিনশট:
সফটওয়্যার বিবরণ:
Hol সংক্ষিপ্ত উচ্চ আদেশ যুক্তিবিজ্ঞান থেকে উপপাদ্য প্রমাণ এবং প্রমাণ সরঞ্জাম প্রয়োগ করা যেতে পারে, যা একটি প্রোগ্রামিং পরিবেশ.
অন্তর্নির্মিত সিদ্ধান্ত পদ্ধতি এবং উপপাদ্য provers স্বয়ংক্রিয়ভাবে অনেক সহজ উপপাদ্য স্থাপন করতে পারেন. একটি ওরাকল প্রক্রিয়া যেমন SAT এবং BDD ইঞ্জিন হিসাবে বহিস্থিত প্রোগ্রাম অ্যাক্সেস দেয়.
Hol 4 সিদ্ধান্তগ্রহণ, মৃত্যুদন্ড এবং সম্পত্তি পরীক্ষণ সমন্বয় বাস্তবায়নের জন্য একটি প্ল্যাটফর্ম হিসাবে বিশেষভাবে উপযুক্ত
এই রিলিজে নতুন কি:.
- HolSmtLib এখন লক্ষ্য Z3 প্রমাণ পুনর্গঠন সমর্থন করে নির্দিষ্ট প্রস্থ শব্দ এবং শ্রীমতি-lib 2 বিন্যাসে Hol থেকে একটি অনুবাদ জড়িত.
- HolQbfLib বৈধতা এবং Squolem 2.02 জন্য সার্টিফিকেট দুর্বলতা উভয় জন্য চেক সমর্থন করে. একটি সংখ্যাগত এবং একটি নির্দিষ্ট প্রস্থ শব্দ প্রয়োগ যখন wordsSyntax.mk_word_replicate ফলে শব্দ প্রস্থ নির্ণয় করে.
- সিস্টেম দশমিক ভগ্নাংশ জন্য বাক্য গঠন সমর্থন করে.
- ফর্ম বিভাগ পদ এন / 10 মিটার. এই বাক্য গঠন মানচিত্র
- কোর সিস্টেম, এই বাক্য গঠন, বাস্তব যুক্তিসঙ্গত, এবং জটিল তত্ত্ব জন্য সক্রিয় করা হয়.
সংস্করণ 6 নতুন কি:
- HolSmtLib লাইব্রেরি এখন শ্রীমতি সমাধানকারী Z3 জন্য প্রমাণ পুনর্গঠন সমর্থন .
- অনেক ধরনের ভেরিয়েবল এখন পার্স এবং ছোট হাতের গ্রিক অক্ষর হিসেবে প্রিন্ট করা যাবে.
- Bounded rewrites ভাল কাজ.
- এল অপারেটর জড়িত পদ সরলীকরণ ভাল.
- ব্যাগ অস্ত্রোপচারের জন্য উন্নত সমর্থন.
- সিনট্যাক্স আপডেট.
- অন্যান্য ক্ষুদ্র উন্নতি ও বাগ.
সার্বজনীন সেট ভালো জিনিসের জন্য
পাওয়া মন্তব্যসমূহ না