1215 ورقة بحثية
تقترح هذه الورقة دلالات قائمة على الطبقات لـ "منطق الزمن الإشاري" (STL) توجد علاقة تطابق بين صيغ هذا المنطق والطبقات الزمكانية، مما يوفر إطاراً نظرياً لتحليل وتفسير فضاءات التضمين لوكلاء التعلم التعزيزي العميق، وهو ما تم التحقق من صحته من خلال تطبيقات في ألعاب "ميني جريد" (Minigrid).
تقدم هذه الورقة نظام إثبات تفاعلي قائم على حل النزاعات (resolution) لمسألة عدم القابلية للإرضاء (UNSAT)، يتيح التحقق الفعال دون الحاجة إلى شهادات أسية، حيث تقدم تحديداً أول بروتوكول تفاعلي تنافسي لإجراء "ديفيس-بوتنامم" لحل النزاعات، جنباً إلى جنب مع إطار نظري للأرثمتة (arithmetization) ونتائج تجريبية.
تُبين هذه الورقة أن كل رسم بياني شبه قابل للحساب ضمن فضاء متري قابل للحساب يمكن تقريبه بشكل تعسفي جيد بواسطة رسم بي𝗵اني فرعي قابل للحساب يتميز بنقاط نهاية قابلة للحساب.
تقدم هذه الورقة إطار عمل للتحقق التركيبي من البرامج في نظرية الأنواع المعتمدة، والذي يستخدم الدوال متعددة الحدود لنمذجة الواجهات والتنفيذات والمواصفات، موضحاً كيفية تركيب هذه المكونات عبر مخططات التوصيل وآلات ميلي مع كونها مصاغة بالكامل في لغة أغدا.
تقدم هذه الورقة بروتوكول (Lean-Agent)، وهو نظام تحقق رسمي يستخدم إثبات النظريات عبر لغة (Lean 4) لضمان امتثال إجراءات الذكاء الاصطناعي المالي المستقل للمتطلبات التنظيمية الصارمة رياضياً، مما يستبدل الحواجز الوقائية الاحتمالية غير الكافية بسلامة حتمية وقابلة للتحقق تشفيراً.
تقدم هذه الورقة إطار عمل قائماً على نموذج إرضاء الالتزامات (SAT) لمسألة تقطيع مخزون السلع أحادية حجم السهم ثنائية الأبعاد، والتي تستخدم توسيع الطلب، وإلغاء التوجيه، واستراتيجيات حل متنوعة للتفوق بشكل كبير على الحلول التجارية مثل OR-Tools وCPLEX وGurobi في إثبات المثالية وتقليل الفجوات في النماذج المرجعية.
تُوصّف هذه الورقة القدرة التعبيرية لجزئية المنطق العددي ذات من المتغيرات و من رتبة المكمّم عبر عدم التمييز بالتشاكل على الرسوم البيانية ذات أغطية غابات الـ -pebble بعمق ، وتثبت أن هذه الفئة تختلف عن تقاطع الرسوم البيانية ذات عرض الشجر المحدود والرسوم البيانية ذات العمق الشجري المحدود، وتؤكد حدسية روبرتسون بأن هذه الفئات مغلقة تحت التمييز بالتشاكل من خلال تحليل جديد للعبة "الشرطي واللص" الرتيبة.
تقدم هذه الورقة مفهوم التعددات الشكلية الكمومية لإنشاء إطار جبري لمسائل الالتزام بالقيود الكمومية، مع توصيف كامل لأدوات التبديل وإثبات عدم قابلية التقرير لبعض مسائل الالتزام بالقيود الكمومية، بما في ذلك تلك المحددة بمعاملات الدورات الفردية وبنود سيغرز.
تقترح هذه الورقة نموذجاً هيكلياً موحداً (metamodel) للأنظمة المعلوماتية المدفوعة بنماذج اللغات الكبيرة (LLM)، يعمل على تنظيم المخططات الهيكلية الرئيسية عبر طبقات الأعمال، والنظام، والمطورين، لتمكين تحويلات مستقرة، ومتكررة، وعالية الجودة بين الكود والوثائق.
تقدم هذه الورقة إطارًا معياريًا وحسابات تسلسل سليمة وكاملة لمنطق (STIT) الواجب، والذي يصيغ ويقارن ويحلل العلاقات المنطقية بين عشرة تفسيرات متميزة لمبدأ "الواجب يستلزم الاستطاعة".