مينلوج
MINLOG هو مساعد إثبات تم تطويره في جامعة لودفيغ ماكسيميليان في ميونخ بواسطة فريق هيلموت شفيتشتنبرغ . [ 1 ] [ 2 ]
يعتمد نظام MINLOG على حساب الاستدلال الطبيعي من الدرجة الأولى . وهو مصمم للاستدلال حول الدوال القابلة للحساب ، باستخدام المنطق الأدنى بدلاً من المنطق الكلاسيكي أو الحدسي . الدافع الرئيسي وراء MINLOG هو استغلال نموذج "البراهين كبرامج" لتطوير البرامج والتحقق منها. في الواقع، تُعامل البراهين ككائنات من الدرجة الأولى، قابلة للتطبيع. إذا كانت الصيغة وجودية، فيمكن استخدام برهانها لقراءة مثال منها أو تعديله بما يتناسب مع تطوير البرامج من خلال تحويل البرهان. ولتحقيق هذه الغاية، زُوّد MINLOG بأدوات لاستخراج البرامج الوظيفية مباشرةً من مصطلحات البرهان. وينطبق هذا أيضًا على البراهين غير البنائية، باستخدام ترجمة A مُحسّنة . يدعم النظام البحث التلقائي عن البراهين والتطبيع عن طريق التقييم كأداة فعالة لإعادة كتابة المصطلحات .
مراجع
- ↑ فيزنت، فرانزيسكوس (25 أبريل 2018). "مقدمة في مينلوغ" . البرهان والحساب . وورلد ساينتيفيك: 233-288 . doi : 10.1142/9789813270947_0008 . ISBN 978-981-327-093-0تم الاطلاع عليه بتاريخ 15 فبراير 2025 .
- ^ "المنطق الرياضي - www.minlog-system.de" . www.mathematik.uni-muenchen.de . جامعة لودفيغ ماكسيميليان في ميونيخ . تم الاسترجاع في 15 فبراير 2025 .
روابط خارجية
- مساعدو التدقيق اللغوي
- نماذج أولية للأساليب الرسمية