1215 ورقة بحثية
تقدم هذه الورقة فئات ذات نواتج ثنائية محدبة لإنشاء حساب قائم على المصفوفات العشوائية وإطار رسومي للإعدادات الاحتمالية، مما يوفر في النهاية صياغة بديهية كاملة للدوائر البولينية الاحتمالية.
تقدم هذه الورقة منطق تبرير حيث يتم تحديد مصطلحات الإثبات صراحةً بمصطلحات لامدا () النوعية، مما يوفر صياغة استنباطية، ونظام استنتاج طبيعي، وحساب تسلسل (sequent calculus) يقضي بحذف القطع لتوحيد الاستدلال حول الحوسبة والإثبات تحت تقابل كوري-هوارد.
تقدم هذه الورقة اشتقاقاً آلياً بالكامل لخوارزمية توحيد ثلاثية الوسائط باستخدام التركيب الاستنتاجي للبرامج، مما يعمم ويؤتمت برهاناً يدوياً لـ "مانا ووالدنجر" لتوليد برنامج صحيح يحسب الموحدات الأكثر عمومية وتكراراً (idempotent) بالنسبة لتعويض بيئة تراكمية.
تستعرض هذه الدراسة المسحية بشكل منهجي تقنيات تحليل إنهاء البرامج ذات القيود الخطية، حيث تغطي نتائج القابلية للتقرير التأسيسية، ودوال التصنيف، وثوابت الانتقال الارتكازية الموزعة، مع فحص المقايضات بين القدرة التعبيرية والتعقيد الحسابي، وإن كانت تستبعد اللغات الواقعية والنماذج الأكثر تعقيداً مثل الحساب غير الخطي أو الاختيار الاحتمالي.
تقدم هذه الورقة شبكات البوابات المنطقية المرتبطة بالمدخلات (IALGNs)، وهي بنية مبتكرة تتغلب على قيود قابلية التوسع في العمق لشبكات البوابات المنطقية التقليدية من خلال ربط كل طبقة بالمدخل الأصلي، مما يتيح تحسيناً مستقراً للنماذج وتحسناً متسقاً في الدقة عبر الشبكات التي تتجاوز 100 طبقة.
تقدم هذه الورقة البحثية dGL3، وهو منطق ألعاب تفاضلية لثلاثة لاعبين مع حساب برهان سليم وكامل نسبياً مصمم للتحقق من الألعاب الهجينة غير الصفرية حيث يمكن للاعبين ذوي الأهداف الفردية تشكيل تحالفات، مما يتغلب على القيود المفرطة في التحفظ لافتراضات المجموع الصفري في السيناريوهات التي تتضمن أهداف سلامة مشتركة.
تقدم هذه الورقة صياغة في لغة Lean 4 لخوارزمية Kannan-Bachem للنمط القياسي لـ Smith للمصفوفات الصحيحة غير المنفردة، مع توفير براهين مثبتة آلياً على صحتها وتحديد حدود حدودية ثابتة لكل من التعقيد الحسابي لعدد البتات للحوسبة وحجم مخرجاتها.
تقدم هذه الورقة ProofWala، وهو إطار عمل متعدد اللغات مبني على مكتبة قابلة لإعادة الاستخدام للتفاعل البرمجي مع مبرهنات التفاعل التي تتيح استخراج بيانات برهنة وفحصاً متوازياً يتسمان بالقدرة على التوسع والأمانة الدلالية، مما يثبت أن التدريب عبر اللغات بين Lean وRocq يحسن بشكل كبير أداء إثبات النظريات والتكيف مع المجالات.
توسع هذه الورقة نموذج الـ presheaf الامتدادي للتعاود المحروس متعدد الساعات إلى أعداد ترتيبية أعلى، مما يتيح تفسيرات نظرية للمجموعات تتحقق من صحة ترميزات الأنواع التعاونية المعقدة التي تتضمن المجموعات الجزئية المتناهية، والتوزيعات، والكم الوجودي.
تقدم هذه الورقة ترجمة شبيهة بترجمة تسيتين (Tseitin-like translation) تعمل على اختزال الصيغ الزمنية المترية التعسفية إلى جزء من برنامج منطقي يقتصر على معاملات الماضي، مما يتيح استخدام برامج حل برمجة المجموعات الجوابية (ASP) الموجودة للاستدلال بشأن قيود التوقيت الكمي في منطق التوازن الزمني المتري.