1215 ورقة بحثية
تقترح هذه الورقة نهجاً جديداً للتحقق الرسمي من أمن الاستقصاء للخوارزميات التشفيرية المقنعة عبر الاستفادة من منطق الفصل الاحتمالي (Lilac) لإقامة صلة بين خصائص عدم التداخل والاستقلال الشرطي.
تُثبت هذه الورقة أن نتائج الاستحالة من نوع "آرو" في تجميع الأحكام تبرز مجددًا حتى عند قصرها على أحكام جهوية حقيقية، مما يثبت أن البنى الدلالية الجهوية المحددة وحدها يمكن أن تولد الترابطات المنطقية اللازمة للاستبداد دون الاعتماد على قضايا واقعية مقنعة.
تقدم هذه الورقة أول برهان آلي لخاصية الحيوية (liveness) لأنواع الجلسات متعددة الأطراف المتزامنة في مساعد الإثبات Rocq، وذلك باستخدام الأشجار والعلاقات التعاونية (coinductive trees and relations) للتحقق رسميًا من سلامة وحيوية بروتوكولات الاتصال من خلال ما يقرب من 14,000 سطر من الكود البرمجي.
تقدم هذه الورقة البرمجة المنطقية لتعيين المجموعات العشوائية (SQASP) كأول نهج قائم على برمجة تعيين المجموعات (ASP) لحل ألعاب لغة وصف الألعاب العامة (GDL) ذات لاعبين بنظام تبادل الأدوار مع وجود عدم يقين، مما يثبت تنافسيتها مع البحث الأمامي في الألعاب العشوائية الصغيرة وإمكاناتها في تقييم نهاية اللعبة.
تُثبت هذه الورقة وجود ثلاثية تعقيد كاملة (Logspace، أو NP-complete، أو PSpace-complete) لمسألة الالتزام المقيد المكممة (QCSP) فوق لغات التساوي، وذلك من خلال إثبات أن هي مسألة PSpace-complete، مع تصنيف متغير التناوب المحدود ضمن الهرم متعدد الحدود (Polynomial Hierarchy).
تثبت هذه الورقة أنه لا يمكن لأي طريقة لترتيب الميزات أن تحقق الأمانة والاستقرار والكمال في آن واحد في ظل وجود التلازم بين الميزات، حيث تصف حيز التصميم الناتج كفصل حاد بين الطرق الأمينة غير المستقرة والأساليب التجميعية مثل DASH، مع التحقق ميكانيكيًا من جميع النتائج في لغة Lean 4.
تعمم هذه الورقة خاصية الطول المحدود للمجموعة النقية القابلة للعد والترتيب الخطي الكثيف على فئة واسعة من البنى اللانهائية، بما في ذلك رسم رادو البياني، وذلك عبر إرساء شروط تعتمد على أعداد المدارات في المميز صفر والدمج الحر في المفردات المتناهية، مع استكشاف الروابط مع فضاءات الدوال والآلات ذاتية التشغيل أيضاً.
تقدم هذه الورقة البرامج المنطقية النمطية البارامترية كصيغة جديدة لبرمجة مجموعات الإجابات من الدرجة الأولى تدعم البارامترات والداخلية، مما يوفر أساساً نظرياً لالتقاط دلالات ميزة التحكم الجماعي في clingo والجسر بين البرمجة المنطقية النمطية والتقليدية غير النمطية.
تضع هذه الورقة شروطاً ضرورية وكافية للتوليد المحدود للمثاليّات متعددة الحدود المتكافئة فوق البنى المنطقية المعدودة، وتطوّر خوارزمية "بوخبير" موسعة لحساب قواعد "غروبنر" الخاصة بها، مما يحل مشكلة العضوية ويُمكّن من التطبيقات في مجالات مثل أوتوماتا السجلات وشبكات "بتري" مع البيانات.
تقدم هذه الورقة منطقاً كمياً من الرتبة العليا أفينياً (affine) مزوداً بمبادئ استقراء وعود (recursion) محروسة جديدة للفضاءات المترية كاملة التمام ومحدودة بـ $1$ وتدابير الاحتمال، مما يبرهن على فائدته في التحقق من البرامج والعمليات الاحتمالية من خلال دراسات حالة حول مسافات التشابه (bisimilarity distances)، وتقارب التعلم الزمني، والمسارات العشوائية.