أمينة دومان (من مواليد 2 سبتمبر 1990) عالمة حاسوب ونظرية مغربية،[2] فازت بجائزة أفضل رسالة دكتوراه بفرنسا حملت عنوان «نظرية إثبات لا مركزية المنطق والنقاط الثابتة». رائدة في إثبات نظرية مهمة في المنطق الرياضي، وهي نظرية الاكتمال في حساب التفاضل والتكامل الخطي، وذلك بطريقة بناءة ( أي عن طريق إنتاج شهادة). من خلال هذا العمل، قامت بسد الفجوة بين المنطق الرياضي والتحقق من الخصائص اللانهائية للبرمجيات، مما يسمح بالاستدلال بشكل استقرائي وتوافقي.
دومان حصدت جائزة «جيل كان» (Prix Gilles-Kahn) بقيمة 1500 أورو عن أطروحتها، التي وضعت بالمرتبة الأولى بين أفضل الأطروحات الفرنسية.
وقد سبق لدومان أن حصلت على زمالة عام 2014 في مجال اهتمامها بالرياضيات من لدن مؤسسة "DIM Math Innov".[3][4]
فازت خلال عام 2017 بجائزة جايلز كان الفرنسية لأفضل أطروحة دكتوراه في فرنسا. كانت أطروحتها حول موضوع نظرية البرهان اللانهائي للمنطق بالنقاط الثابتة. حيث تظهر أطروحتها أن البراهين الدائرية لها مكانة حقيقية كدليل نظري وأنه يمكن تطبيقها على مجالات أخرى مثل التحقق الرسمي.[5] في 31 يناير 2018، حصلت دومان على الجائزة من جمعية علوم الكمبيوتر الفرنسية (SIF).[6]
السيرة
أمينة دومان من مواليد يوم الأحد 2 سبتمبر 1990[7] بالمغرب.[8]
أكملت دراستها الثانوية بمدرسة الشروق الثانوية بخريبكة حيث حصلت على البكالوريا العلمية بتقدير جيد جدا سنة 2008. ومثلت المغرب في الأولمبياد الدولي للرياضيات ثم التحقت بالصفوف الإعدادية بمدرسة ابن عبدون بخريبكة قبل أن تدخل MP* " المواد الإجبارية الرياضيات والفيزياء الصف الاعدادي" بمدرسة مولاي يوسف الثانوية بالرباط.
وفي عام 2010، التحقت بالمدرسة المركزية بباريس، وتخصصت في الرياضيات التطبيقية.
في عام 2014، استفادت أمينة دومان من منحة دراسية من منطقة إيل دو فرانس كجزء من مجال الاهتمام الرئيسي "أبحاث الدكتوراه في الرياضيات-IDF"، منذ إعادة تسميتها ديم الرياضيات إينوف "DIM Math Innov".[8]
وفي الفترة من 2014 إلى 2017، أعدت أطروحتها للدكتوراه بعنوان حول نظرية البرهان اللانهائي للمنطق بالنقاط الثابتة،[9] والتي أشرف عليها ديفيد بيلد، وبيير لويس كوريان، وألكسيس سورين في جامعة باريس ديدرو.
عملت منذ ذلك الحين كباحثة ما بعد الدكتوراه في جامعة وارسو مع ميكوواج بويانتشيك وفي مختبر علوم الكمبيوتر الموازي (LIP) في ENS ليون مع داميان بوس.
أبرز أعمالها
يقع عمل أمينة دومان في إطار نظرية البرهان.[2]
تستخدم المنطق اللامتناهي من بين أمور أخرى للتحقق من برامج الكمبيوتر، مما يسمح بصيغ أو عروض توضيحية طويلة بشكل لا نهائي.
النتيجة التي تم الحصول عليها تتعلق بـ "نظرية الاكتمال". وتقول أمينة أنه إذا كانت الصيغة صحيحة فهي قابلة للإثبات. وقد قدم الأمريكي ديكستر كوزين عام 1983 ومن ثم روب كايفولا[10] عام 1995 برهانًا على هذه النظرية في إطار حساب التفاضل والتكامل ولكن بطريقة غير بناءة،[alpha 1] أي أننا علمنا أن الدليل موجود لكننا لم نتمكن من إنتاج هذا الدليل.
يتيح عمل أمينة دومان الآن التصديق على أن نظام الكمبيوتر يلبي المتطلبات المحددة له ومع إنتاج الشهادة التي تثبت ذلك. "الشهادة هي تعبير رياضي ودليل على هذا التضمين الذي يمكن توصيله إلى أشخاص آخرين، بالإضافة إلى ذلك سيعرفون سبب استيفاء النظام للخاصية: الشهادة لها فضيلة تفسيرية" على حد تعبير الباحث.
ولتحقيق ذلك نجحت أمينة دومان في تصميم خوارزمية تسمح ببناء البرهان تلقائيًا من صيغة حسابية.[11] كما يمكن أن تكون صيغة حساب التفاضل والتكامل هذه "المعنى الضمني الكبير" الذي يعبر عن أن النظام (S) يلبي الخاصية (P)، أي أن (S) ⇒ (P) صحيح. للحصول على البرهان البناء يتم تحليل أي صيغة حسابية إلى صيغ فرعية متوسطة، ثم يتم إثبات كل منها باستخدام البراهين اللانهائية. وأخيرًا تطبق على كل من هذه البراهين خوارزمية طورتها مما يجعل من الممكن تحويل برهان لا نهائي إلى برهان عادي. حيث تكمن الصعوبة في اختيار التحليلات. ولتحقيق ذلك استلهمت فكرة الأوتوماتا التي توفر أدوات للتغلب على صعوبات التناوب (∧ و∨)، وشروط التكافؤ (تناوب μ وν) وعدم الحتمية (وجود ∨).[12]
المنشورات
- لها حول نظرية البرهان اللامتناهي للمنطق بالنقاط الثابتة عام 2017 أطروحة تمت مناقشتها في جامعة باريس ديدرو (باريس 7) السوربون باريس سيتي وتم إعدادها في معهد البحوث في علوم الكمبيوتر الأساسية (IRIF) وفي مختبر المواصفات والتحقق ( LSV) تحت إشراف ديفيد بيلدي وأليكسيس سورين وبيير لويس كورين. حيث تمحورت أطروحتها للدكتوراه حول نظام البرهان الدائري.
- الاكتمال البناء لحساب التفاضل والتكامل للزمن الخطي، 2017 DOI:10.1109/LICS.2017.8005075
مرتبة الشرف والأوسمة والجوائز والامتياز
جائزة جيل خان لأفضل أطروحة دكتوراه فرنسية، 2017، من قبل شركة المعلوماتية الفرنسية " Société informatique de France (SIF)".[13]
الملاحظات والمراجع
ملاحظة
- ^ R. Kaivola démontre le théorème de complétude du μ-calcul : « Si une formule du μ-calcul est valide, alors elle est prouvable dans le système de Kozen ».
