1215 ورقة بحثية
تُثبت هذه الورقة أن قصر بروتوكولات البث غير الحاصرة على خاصية "الانتظار فقط" يقلل من التعقيد الحسابي لمشكلات تغطية الحالة والتكوين من درجة "أكرمان-صعبة" إلى "P-كاملة" و"PSPACE-كاملة" على التوالي.
تقدم هذه الورقة "مسألة الإيجابية" للمتتاليات شبه الخطية التكرار، وهي تعميم للمتتاليات الخطية التكرار، وتقدم إجراء قرار للحالات من الدرجة الثانية مدعوماً بنتيجة تجاوز جديدة للمتسلسلات اللانهائية.
تقدم هذه الورقة أول نموذج أولي متاح للجمهور للمراقبة الكمية عبر الإنترنت لمنطق الإشارة من الدرجة الأولى (SFO) من خلال تعريف دلالات قائمة على المتانة، وتحويل صيغ الاستجابة المحدودة إلى جزء من زمن الماضي يمكن مراقبته بكفاءة، وإثبات عملية هذا النهج من خلال تقييمات معيارية.
تحل هذه الورقة البحثية المشكلة المفتوحة المتعلقة بحدود تعميم الطول القابلة للحوسبة لنماذج المحولات (transformers) من خلال إثبات أن مثل هذه الحدود غير قابلة للحوسبة لنموذج CRASP (وبالتالي للمحولات العامة) باستخدام طبقتين فقط، مع وضع حدود أسية مثالية للجزء الإيجابي من نموذج CRASP والمحولات ذات الدقة الثابتة.
تقدم هذه الورقة طريقة "قابلية التقريب بمتغير-e" لإنشاء متغيرات-e لفئات التوزيع الشائعة، وتوضح كيف تؤدي عمليات البناء هذه إلى اختبارات عشوائية صريحة قائمة على مفهوم ليفين من نظرية المعلومات الخوارزمية.
يجمع هذا المجلد مقالات لزملاء ومؤلفين مشاركين لستيفانو بيراردي للاحتفاء بمسيرته المهنية وتسليط الضوء على التطورات الأخيرة في نظرية البرهان ونظرية النوع، لا سيما في المنطق البنائي، والأنواع المعتمدة، والبراهين الدورية.
تقدم هذه الورقة برهاناً جديداً لمبرهنة تشوبريتش (Čubrić) الخاصة بالاستكمال ذي الصلة بالبرهان (proof-relevant interpolation theorem) لحساب لامدا بسيط النوع (simply-typed lambda-calculus) باستخدام مبادئ النوع ثنائي الاتجاه (bidirectional typing principles)، وتوفر صياغتها الرسمية في مساعد الإثبات روك (Rocq).
تقدم هذه الورقة "فيزياء الفضاء للذكاء الاصطناعي"، وهي إطار دلالي تكويني يعيد تصنيف التوسع السطحي للسلطة كحدث حدودي من الدرجة الأولى يتطلب بروتوكولات شهادة ووساطة محددة لحكم مؤسسات الذكاء الاصطناعي المستمرة وذاتية التوسع.
تقدم هذه الورقة نهجاً نموذجياً للتسلسل في المنطق الخطي عبر تعميم مبرهنة "يو" للرسوم البيانية ذات الألوان المحلية، باستخدام لمّا "تقليل القمم" لاستخراج رؤوس الانقسام واستعادة اشتقاقات حساب الاستنتاج من شبكات البراهين دون تغيير بنيتها الرسومية الأساسية.
تضع هذه الورقة بديهيات الدلالات الفئوية لنظرية النوع المعتمد بالكامل داخل الفئة القياسية للدوال متعددة الحدود، وذلك عبر توظيف نظرية النوع المتجانسة (Homotopy Type Theory) لتعريف "الأكوان متعددة الحدود" كبنى أحادية الوحدة (univalent structures) تستوفي بطبيعتها التماسكات العليا وتُبسّط نظرية النماذج الطبيعية.