لغة البرمجة “إيزابيل” (Isabelle) هي مساعدة دليل عامة للأدلة. تسمح بتعبير الصيغ الرياضية بلغة رسمية وتوفر أدوات لإثبات تلك الصيغ في حسابات منطقية. تم تطوير إيزابيل في الأصل في جامعة كامبريدج وجامعة تقنية ميونيخ، ولكنها الآن تشمل مساهمات عديدة من مؤسسات وأفراد في جميع أنحاء العالم.
تظهر إيزابيل لأول مرة في عام 1986، وهي تعتبر من اللغات ذات المفتوح المصدر، ويمكن الوصول إليها من خلال موقعها الرسمي هنا.
تعتبر إيزابيل من مساعدي الأدلة التفاعلية، حيث تقدم أدوات فعالة لإثبات النظريات بشكل تفاعلي. تستخدم لغة إيزابيل ميتالوجيك (نوع نظري ضعيف) لتشفير اللغات الكائنية مثل المنطق من المرتبة الأولى، والمنطق من المرتبة العالية، ونظرية مجموعات زيرميلو-فرينكل (ZFC).
أحد أساليب الإثبات الرئيسية في إيزابيل هو نسخة من القرار من المرتبة العالية، والذي يعتمد على توحيد من المرتبة العالية. على الرغم من التفاعلية، تضم إيزابيل أيضًا أدوات فعالة للتفكير التلقائي، مثل محرك إعادة الكتابة ومثبت الجداول، بالإضافة إلى عدة إجراءات لاتخاذ القرار.
تم استخدام إيزابيل لتشكيل العديد من النظريات في الرياضيات وعلوم الحاسوب، مثل نظرية اكتمال جودل، ونظرية جودل حول اتساق مبدأ الاختيار، ونظرية الأعداد الأولية، وصحة بروتوكولات الأمان، وخصائص دلالة لغات البرمجة.
تمتاز إيزابيل بأنها مجانية ومفتوحة المصدر، ويمكن استخدامها وتعديلها وتوزيعها بموجب رخصة BSD المنقحة.
تمت إطلاق إيزابيل بعد اسم ابنة جيرار هيوت من قبل لورانس بولسون.
يمكنك الحصول على مزيد من المعلومات حول إيزابيل عبر صفحتها على ويكيبيديا هنا.
إيزابيل لديها ميزات متعددة، مثل وجود تعليقات في الكود وعدم وجود تنسيق ذاتي للتعليقات البصرية ولكنها تدعم بنية جملة معينة، وعدم وجود تعليقات خطية. تتميز بكونها ذات شفرة مفتوحة وتدعم مستودعات الحزم المركزية.
بالنظر إلى أماكن الأصل، فإن جامعة كامبريدج وجامعة تقنية ميونيخ هما المجتمع الرئيسي الذي أسهم في تطوير إيزابيل.
يمكن أن تحتوي ملفات إيزابيل على امتداد .thy وهي من نوع النصوص.
هذه بعض المعلومات الأساسية والشاملة عن لغة البرمجة إيزابيل.