إيزابيل (مساعدة التدقيق)

📅 آخر تحديث: ٣١ يوليو ٢٠٢٦
✍️ نُشر في: ٣١ يوليو ٢٠٢٦
الموسوعة الحرة

برنامج Isabelle [ a ] الآلي لإثبات النظريات هو برنامج لإثبات النظريات يعتمد على منطق الرتبة العليا (HOL) ، مكتوب بلغة Standard ML و Scala . وباعتباره برنامجًا لإثبات النظريات على نمط منطق الدوال القابلة للحساب (LCF)، فهو يعتمد على نواة منطقية صغيرة (kernel) لزيادة موثوقية البراهين دون الحاجة إلى كائنات إثبات صريحة، مع دعمها في الوقت نفسه.

يتوفر نظام إيزابيل ضمن إطار عمل مرن يسمح بتوسيعات آمنة منطقيًا، تشمل النظريات والتطبيقات لتوليد الشفرة وتوثيقها، بالإضافة إلى دعم خاص لمجموعة متنوعة من الأساليب الرسمية . ويمكن اعتباره بيئة تطوير متكاملة (IDE) للأساليب الرسمية. في السنوات الأخيرة، جُمع عدد كبير من النظريات وتوسيعات النظام في أرشيف إيزابيل للبراهين الرسمية ( Isabelle AFP ). [ 2 ]

أطلق لورانس بولسون اسم إيزابيل على ابنة جيرار هويه . [ 3 ]

برنامج إثبات نظرية إيزابيل هو برنامج مجاني ، تم إصداره بموجب ترخيص BSD المعدل .

سمات

إيزابيل لغة عامة: فهي توفر منطقًا فوقيًا ( نظرية أنواع ضعيفة )، يُستخدم لترميز منطق الكائنات مثل منطق الرتبة الأولى (FOL) ومنطق الرتبة العليا (HOL) ونظرية مجموعات زيرميلو-فرانكل (ZFC). يُعد منطق الكائنات الأكثر استخدامًا هو إيزابيل/HOL، على الرغم من أن تطورات مهمة في نظرية المجموعات قد أُنجزت في إيزابيل/ZF. تعتمد طريقة الإثبات الرئيسية في إيزابيل على نسخة من الرتبة العليا من الاستدلال ، استنادًا إلى التوحيد من الرتبة العليا .

على الرغم من كونها تفاعلية، تتميز إيزابيل بأدوات استدلال تلقائي فعّالة، مثل محرك إعادة كتابة المصطلحات ومُثبت الجداول ، وإجراءات اتخاذ قرارات متنوعة، ومن خلال واجهة أتمتة إثبات Sledgehammer ، توفر حلولًا خارجية لإمكانية الإرضاء المعياري للنظريات (SMT) (بما في ذلك CVC4 ) ومثبتات نظرية آلية قائمة على الاستدلال (ATPs)، بما في ذلك E و SPASS و Vampire ( تعيد طريقة إثبات Metis [ b ] بناء براهين الاستدلال التي تولدها هذه المثبتات). [ 4 ] كما أنها تتميز بمكتشفين للنماذج ( مولدات الأمثلة المضادة ): Nitpick [ 5 ] و Nunchaku . [ 6 ]

تتميز لغة إيزابيل بوحدات محلية (locales) وهي وحدات تقوم بتنظيم البراهين الكبيرة. تحدد الوحدة المحلية الأنواع والثوابت والافتراضات ضمن نطاق محدد [ 5 ] بحيث لا يتعين تكرارها لكل لمة .

Isar (" الاستدلال شبه الآلي المفهوم ") هي لغة الإثبات الرسمية لإيزابيل. وهي مستوحاة من نظام ميزر . [ 5 ]

برهان مثال

تتيح لغة إيزابيل كتابة البراهين بأسلوبين مختلفين: الإجرائي والتصريحي . تحدد البراهين الإجرائية سلسلة من التكتيكات (دوال /إجراءات إثبات النظريات ) التي يجب تطبيقها. ورغم أنها تعكس الإجراء الذي قد يتبعه عالم الرياضيات لإثبات نتيجة ما، إلا أنها عادةً ما تكون صعبة القراءة لأنها لا تصف نتائج هذه الخطوات. يُعتبر هذا الأسلوب "ضارًا" في وثائق إيزابيل. [ 7 ]

من ناحية أخرى، تحدد البراهين التصريحية (المدعومة بلغة برهان إيزابيل، Isar) العمليات الرياضية الفعلية التي سيتم تنفيذها، وبالتالي يسهل قراءتها والتحقق منها من قبل البشر.

على سبيل المثال، يمكن كتابة برهان تصريحي بالتناقض في Isar على أن الجذر التربيعي للعدد اثنين ليس عددًا نسبيًا على النحو التالي.

نظرية جذر 2 ليس عددًا نسبيًا: "جذر 2 ∉ ℚ" . البرهان: ليكن ?x = "جذر 2". لنفترض أن "?x ∈ ℚ". إذن، نحصل على mn :: عدد طبيعي حيث جذر_النسبة: "¦?x¦ = m / n" وأدنى_الحدود : "أعداد أولية فيما بينها m و n" . باستخدام ( قاعدة Rats_abs_nat_div_natE)، ومن ثم "m^2 = ?x^2 * n^2". باستخدام (auto simp add: power2_eq_square)، ومن ثم المعادلة : "m^2 = 2 * n^2". باستخدام of_nat_eq_iff_power2_eq_square، ومن ثم "2 dvd m^2" . باستخدام simp، ومن ثم "2 dvd m"، ومن ثم "2 dvd n" . البرهان: من ‹ 2 dvd m› نحصل على k حيث "m = 2 * k" . باستخدام المعادلة، نحصل على "2 * n^2 = 2^2 * k^2" بالتبسيط، ومن ثم "2 dvd n^2" بالتبسيط ، وبالتالي "2 dvd n" بالتبسيط ، وهو المطلوب إثباته. مع ‹2 dvd m› لدينا "2 dvd gcd m n" (باستخدام قاعدة gcd_greatest). مع lowest_terms لدينا "2 dvd 1" بالتبسيط ، وبالتالي خطأ. باستخدام odd_one ( باستخدام blast )، وهو المطلوب إثباته.

التطبيقات

تم استخدام إيزابيل للمساعدة في الأساليب الرسمية لتحديد وتطوير والتحقق من أنظمة البرمجيات والأجهزة.

استُخدمت إيزابيل لصياغة العديد من النظريات في الرياضيات وعلوم الحاسوب ، مثل نظرية غودل للاكتمال ، ونظرية غودل حول اتساق بديهية الاختيار ، ونظرية الأعداد الأولية ، وصحة بروتوكولات الأمان ، وخصائص دلالات لغات البرمجة . وكما ذُكر، فإن العديد من البراهين الرسمية محفوظة في أرشيف البراهين الرسمية، الذي يحتوي (حتى عام 2019) على 500 مقالة على الأقل، تضم أكثر من مليوني سطر من البراهين. [ 8 ]

  • في عام ٢٠٠٩، أنتج مشروع L4.verified في NICTA أول برهان رسمي على صحة وظائف نواة نظام تشغيل للأغراض العامة: [ ٩ ] نواة seL4 ( الطبقة الرابعة المدمجة الآمنة ) . تم بناء البرهان والتحقق منه في Isabelle/HOL، ويتألف من أكثر من ٢٠٠,٠٠٠ سطر من نص البرهان للتحقق من ٧,٥٠٠ سطر من لغة C. يشمل التحقق الكود والتصميم والتنفيذ، وتنص النظرية الرئيسية على أن كود C يُنفذ المواصفات الرسمية للنواة بشكل صحيح. كشف البرهان عن ١٤٤ خطأً في إصدار مبكر من كود C لنواة seL4، ونحو ١٥٠ مشكلة في كل من التصميم والمواصفات.

البدائل

توفر العديد من اللغات والأنظمة وظائف مماثلة:

ملحوظات

  1. ↑ / ˌ ɪ z ə ˈ b ɛ l /
  2. ↑ / ˈ miː t ɪ s /​

مراجع

  1. ↑ بولسون، إل سي (1986). "الاستنتاج الطبيعي كحل من الرتبة العليا". مجلة البرمجة المنطقية . 3 (3): 237-258 . arXiv : cs/9301104 . doi : 10.1016/0743-1066(86)90015-4 . S2CID 27085090 . 
  2. ^ إيبرل ، مانويل. كلاين، جيروين. نيبكو، توبياس؛ بولسون, لاري ; ثيمان، رينيه. "أرشيف البراهين الرسمية" . تم الاسترجاع في 1 مايو 2021 .
  3. ↑ غوردون، مايك (16 نوفمبر 1994). "1.2 التاريخ" . إيزابيل وهول . أبحاث كامبريدج للواقع المعزز (مجموعة الاستدلال الآلي). مؤرشف من الأصل في 5 مارس 2017. تم الاسترجاع في 28 أبريل 2016 .
  4. ↑ Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow, "Automatic Proof and Disproof in Isabelle/HOL" Archived 2021-10-15 at the Wayback Machine , in: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.), International Symposium on Frontiers of Combining Systems – FroCoS 2011 , Springer, 2011.
  5. 1 2 3 Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach, "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality" , Journal of Automated Reasoning 61 :333–365 (2018).
  6. ↑ أندرو رينولدز، جاسمين كريستيان بلانشيت، سيمون كروانيس، سيزار تينيلي، "إيجاد النموذج للوظائف المتكررة في SMT" ، في: نيكولا أوليفيتي، أشيش تيواري (محرران)، المؤتمر الدولي المشترك الثامن حول الاستدلال الآلي ، سبرينغر، 2016.
  7. ^ ونزل ، مكاريوس (13 مارس 2025). “الدليل المرجعي لإيزابيل/إيزار” (PDF) . تم الاسترجاع 2025-05-10 .الصفحة 148: "يُعتبر تحسين الهدف التعسفي عبر التكتيكات ضارًا". انظر أيضًا القسم 7.3، "التكتيكات: أساليب الإثبات غير المناسبة"، الصفحات 172-175.
  8. ^ إيبرل ، مانويل. كلاين، جيروين. نيبكو، توبياس؛ بولسون, لاري ; ثيمان، رينيه. "أرشيف البراهين الرسمية" . تم الاسترجاع في 22 أكتوبر 2019 .
  9. ↑ كلاين، جيروين؛ إلفينستون، كيفن؛ هايزر، جيرنوت؛ أندرونيك، جون؛ كوك، ديفيد؛ ديرين، فيليب؛ إلكادوي، داميكا؛ إنجلهارت، كاي؛ كولانسكي، رافال؛ نورش، مايكل؛ سيويل، توماس؛ توش، هارفي؛ وينوود، سيمون (أكتوبر 2009). "seL4: التحقق الرسمي من نواة نظام التشغيل" (ملف PDF) . المؤتمر الثاني والعشرون لجمعية ACM حول مبادئ أنظمة التشغيل . بيج سكاي، مونتانا، الولايات المتحدة الأمريكية. الصفحات 207-200 . 
  10. ↑ سترنيشا، روك؛ باركنسون، ماثيو (7 فبراير 2011). "جافا خفيفة الوزن" . أرشيف البراهين الرسمية (طبعة فبراير 2011 ). ISSN 2150-914X . تاريخ الاسترجاع: 25 نوفمبر 2019 .  

للمزيد من القراءة