1215 ورقة بحثية
تقدم هذه الورقة البحثية "التوحيد الأرضي من الدرجة الثانية" (SOGU)، وهو جزء يسمح بمتغير واحد فقط من الدرجة الثانية ولا يسمح بأي متغيرات من الدرجة الأولى، وتثبت أن متغيرته التساوقية مع رموز الدوال التجميعية (ASOGU) غير قابلة للتقرير عن طريق اختزال مسألة هيلبرت العاشرة إليها، مما يؤدي إلى وضع حد أدنى جديد لعدم قابلية التقرير في التوحيد من الدرجة الثانية.
تثبت هذه الورقة أن النظرية المعادلية لحساب العلاقات الموجبة مع الإغلاق المتعدي (PCoR*) هي كاملة لتعقيد EXPSPACE من خلال تقديم مشتقات رسومية تمدد المشتقات القائمة على الكلمات لبناء أتمتة محدودة على التفكيكات المسارية، مستفيدة من خاصية نموذج عرض المسار المحدود خطياً لتقرير التكافؤ.
تقترح هذه الورقة إطار عمل للاستنتاج الاستنباطي القائم على الاتساق، والذي يدمج التنبؤات من نماذج متعددة سابقة التدريب في وقت الاختبار للتخفيف من تدهور الأداء في البيئات الجديدة، محققاً تحسينات ملحوظة في الدقة ومقياس F1 مقارنة بالنماذج الفردية والمجموعات القياسية من خلال اختيار مجموعة فرعية من التنبؤات التي تعظم التغطية مع تقليل التناقضات المنطقية إلى أدنى حد.
تقدم هذه الورقة GRAMPUS، وهي نظرية أنواع نمطية متدرجة تستخدم درجات زمنية لتحديد وجدولة نبضات الكم رسميًا والاستدلال حولها، موفرةً نماذج فئوية ونحوية لإثبات سلامتها واكتمالها.
تثبت هذه الورقة إمكانية تقرير مسألة سكولم (Skolem Problem) لمتتاليات التكرار الخطي فوق الحلقات التبادلية ذات التوليد المحدود وذات الخصائص الموجبة، وذلك من خلال إثبات أن مجموعات أصفارها تشكل اتحادات نهائية قابلة للحساب الفعال لمجموعات -normal، مستفيدةً من التطورات الأخيرة في حل معادلات -unit والمعادلات الخطية فوق الأعداد المستقلة ضربياً.
تقدم هذه الورقة البحثية "تعداد النماذج الموزونة" (WME) كمسألة متميزة على مستوى الحلّال، وتطرح خوارزميات تكميلية قائمة على "التعلم المتأخر لقرار التراجع" (CDCL) تدمج انتشار الأوزان، والتقليم، وتحليل الصراع في كل من أطر التراجع الزمني وغير الزمني بكفاءة لتعداد النماذج الموزونة.
تقدم هذه الورقة صياغة صورية بنائية لأنظمة إعادة الكتابة المجردة في لغة Agda، والتي تلغي المنطق الكلاسيكي من البراهين القياسية، وتُحسّن معايير الإنهاء والاتساق، وتُبرهن على قابليتها للتطبيق من خلال صياغة صورية لحساب لامدا.
تقترح هذه الورقة إطار عمل فعال وقابل للتوسع للمراقبة عبر الإنترنت لمنطق الوقت المتري (Metric Temporal Logic) لكل من سلوكيات الوقت المنفصل والمستمر، وذلك عن طريق بناء شبكات تسلسلية باستخدام تقنية وسم زمني مستقبلي مبتكرة، والتي أظهرت أداءً فائقاً مقارنة بالأساليب الحالية.
تثبت هذه الورقة أن التحقق من الوحدات لأنظمة الوكلاء المتعددين ذات المكدس هو مسألة كاملة من فئة 2EXPTIME بالنسبة لمواصفات ATL، ولكنه مسألة كاملة من فئة 4EXPTIME بالنسبة لمواصفات *ATL، مما يمثل حالة نادرة لمسألة قرار أولية تتجاوز تعقيدها الزمن الأسي الثلاثي.
تقدم هذه الورقة برهاناً أولياً جديداً لخاصية النموذج المحدود لجبر كلين باستخدام أوتوماتا التحويل، مما يثبت تمام جبر كلين بالنسبة للنماذج العلاقاتية المحدودة ويتضمن النتائج السابقة لكل من بالكا، وبرات، وكوزن.