أمينة دومان
أمينة دومان (من مواليد 2 سبتمبر 1990) عالمة حاسوب ونظرية مغربية،[2] فازت بجائزة أفضل رسالة دكتوراه بفرنسا حملت عنوان «نظرية إثبات لا مركزية المنطق والنقاط الثابتة». رائدة في إثبات نظرية مهمة في المنطق الرياضي، وهي نظرية الاكتمال في حساب التفاضل والتكامل الخطي، وذلك بطريقة بناءة ( أي عن طريق إنتاج شهادة). من خلال هذا العمل، قامت بسد الفجوة بين المنطق الرياضي والتحقق من الخصائص اللانهائية للبرمجيات، مما يسمح بالاستدلال بشكل استقرائي وتوافقي.
| أمينة دومان | |
|---|---|
| معلومات شخصية | |
| الميلاد | 2 سبتمبر 1990 (34 سنة)[1] المغرب |
| مواطنة |  المغرب |
| الحياة العملية | |
| المدرسة الأم | جامعة باريس ديديرو المدرسة المركزية باريس |
| المهنة | عَالِمَة حاسوب، ورياضياتية |
| اللغة الأم | الأمازيغية |
| اللغات | العربية، والأمازيغية |
| مجال العمل | منطق رياضي |
| المواقع | |
| الموقع | الموقع الرسمي |
تعديل مصدري - تعديل  | |
دومان حصدت جائزة «جيل كان» (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 ».
- ^ https://perso.ens-lyon.fr/amina.doumane/cv.pdf.
{{استشهاد ويب}}:|url=بحاجة لعنوان (مساعدة) والوسيط|title=غير موجود أو فارغ (من ويكي بيانات) (مساعدة) - ^ ا ب Prix La Recherche 2018 : Prouver à l'aide de l'infini نسخة محفوظة 2024-08-17 على موقع واي باك مشين.
- ^ مغربية تتوج بـ"أحسن أطروحة دكتوراه" في فرنسا نسخة محفوظة 27 مارس 2019 على موقع واي باك مشين.
- ^ Aide à la recherche : Amina Doumane décroche le prix Gilles-Kahn | Région Île-de-France نسخة محفوظة 21 يوليو 2019 على موقع واي باك مشين.
- ^ "Prix de thèse Gilles Kahn et Prix La Recherche pour Amina Doumane". INS2I. 2 يناير 2018. مؤرشف من الأصل في 2023-12-21. اطلع عليه بتاريخ 2021-01-20.
- ^ "Amina Doumane conferred Gilles Kahn Award for best PhD thesis". 23 يناير 2018. مؤرشف من الأصل في 2024-08-20.
- ^ "CV d'Amina Doumane" (PDF). ens-lyon.fr. اطلع عليه بتاريخ 27 août 2019.
{{استشهاد ويب}}: تحقق من التاريخ في:|تاريخ الوصول=(مساعدة) - ^ ا ب "Aide à la recherche : Amina Doumane décroche le prix Gilles-Kahn". www.iledefrance.fr. اطلع عليه بتاريخ 27 août 2019.
{{استشهاد ويب}}: تحقق من التاريخ في:|تاريخ الوصول=(مساعدة) - ^ "Amina Doumane, On the infinitary proof theory of logics with fixed points" (PDF). اطلع عليه بتاريخ 27 août 2019.
{{استشهاد ويب}}: تحقق من التاريخ في:|تاريخ الوصول=(مساعدة) - ^ Roope Kaivola, Axiomatising Linear Time Mu-calculus, 1995.
- ^ "Prix de thèse Gilles Kahn et Prix La Recherche pour Amina Doumane". اطلع عليه بتاريخ 19 juillet 2019.
{{استشهاد ويب}}: تحقق من التاريخ في:|تاريخ الوصول=(مساعدة) - ^ "Support visuel de la soutenance de thèse" (PDF). مؤرشف من الأصل (PDF) في 2023-04-05. اطلع عليه بتاريخ 2024-08-17.
- ^ "Lauréats 2017". La Société informatique de France. مؤرشف من الأصل في 2024-08-20. اطلع عليه بتاريخ 2021-01-20.
