1215 ورقة بحثية
تقترح هذه الورقة طريقة فك ارتباط قائمة على مشكلة إرضاء البوابات المنطقية (SAT) توحد مختلف متغيرات مسألة التزام الوحدات في نماذج قياسية لـ (SAT)، مما يُمكّن خوارزمية واحدة عامة من التفوق على الحلول المتخصصة في كل من جودة الحل والقدرة على التكيف مع متطلبات أنظمة الطاقة المتطورة.
تقدم هذه الورقة مفهوم "حدود القرار الذرية" لإثبات أن ضمان قابلية القبول في وقت التنفيذ في الأنظمة ذاتية القيادة يتطلب هيكلياً دمج تقييم السياسة وانتقال الحالة في خطوة واحدة غير قابلة للتجزئة، حيث إن النماذج المنفصلة عاجزة بطبيعتها عن منع انتهاكات قابلية القبول في البيئات المتزامنة.
يقدم البحث TensorRocq، وهو مجموعة أدوات مُحققة لمساعد الإثبات Rocq، يعمل على سد الفجوة بين البراهين الصورية والاستدلال المخططاتي عبر تحويل حدود الفئات المونودية المتناظرة إلى رسوم بيانية فائقة (hypergraphs) لتمكين التلاعب بالمخططات الخيطية وإعادة الكتابة التساوقية بشكل حدسي.
تنتقد هذه الورقة نظام كارمو وجونز الأكسيومي الأخير للالتزامات الشرطية من خلال إثبات شكل محدود من الانفجار الديؤنتي، بينما تقدم في الوقت ذاته تصنيفاً إيجابياً لجميع النماذج المرضية لأقوى نظام لهما لعام ١٩٩٧ بدلالة عالم ممكن واحد محظور.
تقدم هذه الورقة أول أنظمة متداخلة المتابعات (nested sequent systems) خالية من القطع (cut-free)، وصحيحة وكاملة، لفئة واسعة من المنطق الجهي المكمم مع المساواة وشروط النطاق المتغيرة، وذلك باستخدام قواعد قائمة على التوقيع وقواعد الوصول المحددة بالقواعد النحوية للتعامل مع خصائص الأطر المعقدة مع إثبات الخصائص الجوهرية لنظرية البرهان مثل القابلية للانعكاس (invertibility) وإزالة القطع التركيبية (syntactic cut-elimination).
تقدم هذه الورقة Foxtrot، وهو أول منطق فصل من الرتبة العليا يُمكّن من الإثبات الآلي للتحسين السياقي للبرامج الاحتمالية المتزامنة من الرتبة العليا ذات الحالة المحلية، وذلك عبر دمج مبادئ متقدمة للاستدلال المتزامن والاحتمالي، بما في ذلك اعتماد مبتكر على بديهية الاختيار ضمن إطار عمل Iris.
تُثبت هذه الورقة أن تضمينات التحسين التأسيسية، التي صُممت في الأصل للبرمجة الصحيحة المختلطة، يمكن نقلها مباشرة إلى مهام إرضاء البوليان (SAT) غير الخاضعة للإشراف عن طريق رسم خرائط صيغ (CNF) إلى تمثيل رسم بياني ثنائي الأجزاء مشترك، مما يتيح تجميع الحالات وتحديد التوزيع دون تغييرات هيكلية أو ضبط دقيق خاضع للإشراف.
تقدم هذه الورقة إطار عمل للتعلم الموجه بالنماذج المضادة، مُنفذ في أداة \vmtlc، والذي يعمل على أتمتة التحقق من برامج العميل باستخدام مكتبات معقدة عبر تركيب عقود نمطية أو سياقية تكون كافية لإثبات صحة العميل ومُتحقق منها بواسطة محرك اختبار.
تحدد هذه الورقة الحدود الأساسية للضغط غير الفاقد للمصادر الاستنتاجية من خلال إثبات أنه عندما تُقاس الدقة عبر الحفاظ على الإغلاق المنطقي بدلاً من التساوي الرمزي، فإن دالة المعدل والتشوه تعتمد حصرياً على النواة غير الزائدة للمصدر، مما يجعل النتائج الزائدة غير مرئية لكفاءة الضغط.
تقدم هذه الورقة عرضاً نظرياً متكاملاً وتجسيداً في نظام Isabelle/HOL للتعليقات النوعية الكاملة والحد الأدنى لمصطلحات حساب لامدا متعدد الأشكال من الرتبة الأولى، والذي تم تطويره من خلال سير عمل تعاوني حيث ينتج الوكلاء البشريون والذكاء الاصطناعي البراهين بشكل مستقل، والتي يتم بعد ذلك تحويلها تلقائياً إلى صيغ رسمية وتعميمها بتدخلات من الذكاء الاصطناعي بتوجيه بشري.