1215 ورقة بحثية
تحل هذه الورقة سؤالاً مفتوحاً من خلال إثبات أن مشكلتي الاحتواء وإعادة الكتابة بـ FO لـ فئة Guarded Monotone Strict NP (GMSNP) قابلتان للتقرير بحد علوي قدره 2NEXPTIME، وهو ما تحقق عبر تنقيح التوصيف الموديل-نظري لجمل GMSNP كاتحادات منتهية من مسائل تحقيق القيود (CSPs) فوق بنى -categorical واختزال مسألة الاحتواء إلى مسألة وجود إعادة تلوين.
تقدم هذه الورقة نهجاً جديداً لبرمجة مجموعات الإجابات (ASP) لتحديد البنى الجزيئية من بيانات طيف الكتلة عبر توظيف التمثيلات القانونية لتقييد فضاء البحث، مما يثبت صحته وأداءه المتفوق مقارنة بطرق كسر التماثل والبرامج التجارية الحالية.
تقدم هذه الورقة probLO، وهو امتداد لبرمجة المنطق الخطي يدمج تمثيل وحوسبة الشبكات البايزية من خلال استخدام أساليب متعددة الرؤوس شبيهة بـ Prolog لإعادة بناء الهيكل وتقطيع المنطق الخطي للحسابات الاحتمالية الرقمية الداخلية.
تُطوّر هذه الورقة مراجعة المعتقدات غير المتماسكة عبر تقديم RCbr، وهو امتداد لمنطق Cbr غني بالاستبدال، يتغلب على القيود السابقة لتمكين البناء الصوري لآليات تغيير المعتقد القائمة على التجذر المعرفي ضمن منطقيات عدم الاتساق الصوري.
تثبت هذه الورقة أن القابلية للإثبات في الأنظمة اللانهائية جيدة الترتيب للمنطق الخطي مع النقاط الثابتة، والمفهرسة برتبة أورديال قابلة للحساب ، هي كاملة لمستوى من التسلسل الهرمي فوق الحسابي، وهي نتيجة تم تحقيقها من خلال أسس نظرية إثبات جديدة تشمل حذف القطع والتركيز.
تؤسس هذه الورقة إطارًا فئويًا لنظريات الدوائر من الرتب العليا باستخدام الإثراء والمنتجات المغايرة في المتعددات الفئوية المتناظرة، مبرهنةً أن قوانينها البنيوية تلتقط سمات رئيسية لنظرية الكم من الرتب العليا مع إثبات أن أي نظرية من هذا القبيل تندمج في نظرية الـ profunctors القوية.
تقدم هذه الورقة نظامًا أوليًا يربط بين Agda وVampire ATP من خلال ترجمة التزامات الإثبات عبر جزء هورن متساوي (equational Horn fragment) مشترك، مما يتيح التوليد التلقائي لإثباتات بنائية لخصائص رياضية معقدة كانت تتطلب سابقًا أيامًا من الجهد اليدوي.
تقيم هذه الورقة قدرات الاستدلال الصوري لأربعة نماذج لغوية كبيرة ضمن بيئات اللعب العام، كاشفةً أنه بينما تُظهر النماذج الحالية تقدماً ملحوظاً، فإن أداءها يتدهور مع زيادة تعقيد المهام وعمق الخطوات، وغالباً ما يكون ذلك بسبب أخطاء استدلال محددة مثل القواعد المهلوسة والأخطاء النحوية.
تُثبت هذه الورقة أنه على الرغم من الحدس الأولي الذي يوحي بخلاف ذلك، فإن كل امتداد لحساب لامبكك الكامل التبدلي مع الاختزال أو الإضعاف، والذي يقبل حساب تسلسل فائق خالٍ من القطع، له حد علوي "أكيرماني" أمثل للقابلية للإثبات، ويتحقق ذلك من خلال استغلال تبعيات مستحدثة بين التسلسلات لتجنب القفزة في التعقيد إلى مستويات "أكيرمان" الفائقة.
يقدم هذا البحث أول حساب برهان للاستدلال حول خصائص الحيوية في البرامج المتزامنة تحت نماذج الذاكرة الضعيفة، ممدداً قواعد الاستجابة لمانا وبنويلي عبر دمج عدالة الذاكرة ودوال الترتيب للذاكرة الضعيفة لإثبات خلو خوارزمية قفل التذكرة (Ticket lock) من الجوع رسمياً.