1215 ورقة بحثية
تستعرض هذه الورقة العمليات القابلة للتعريف من الدرجة الأولى على البنى العلاقاتية، مع التركيز على نظريات الترجمة العكسية والتقسيم التي تعبّر عن خصائص المخرجات عبر خصائص المدخلات، مع تطبيقات محددة على العمليات الخالية من المكممات، والعد بمقياس، والتعرف الخوارزمي للبنى ذات عرض الشجرة المحدود أو عرض النقرة المحدود.
تقترح هذه الورقة وتقيم تنفيذًا لإطار عمل CARCASS باستخدام برمجة مجموعات الإجابات (ASP) لتعزيز التعلم التعزيزي العلاقاتي عبر الاستفادة من التمثيلات المنطقية التصريحية لتجريد فضاء الحالة بشكل فعال في مجالات مثل عالم الكتل (Blocks World) وميني جريد (Minigrid).
تؤسس هذه الورقة صلة نظرية تُظهر أن دوال القيمة للسياسات التي تستوفي خصائص -regular تشفر شهادات ستريت (Streett) من نوع "سوبر مارتينجال" (supermartingale)، مما يجسر الفجوة بين التحقق الصوري والتعلم التعزيزي لتمكين التخليق المنهجي للشهادات عبر فضاءات الحالات المتناهية، واللانهائية كعدّية، والمتصلة.
تقدم هذه الورقة إطار عمل "داتالوج" (Datalog) تصريحيًا ينمذج أنواع البيانات المكررة الخالية من التعارض (CRDTs) كبرامج منطقية قابلة للتنفيذ لتمكين التوصيف المنهجي، والتحليل الآلي، والاختبار القائم على الخصائص للتطبيقات التعاونية المعقدة المتزامنة.
تقدم هذه الورقة دراسة منهجية لتخليق الأنظمة ذات الحالة اللانهائية من خلال إرساء طريقة لحل ألعاب التكافؤ المعرفة بمنطق الرتبة الثانية العليا (MSO) واستخلاص استراتيجيات فوز موحدة عديمة الذاكرة.
تقدم هذه الورقة برهاناً احتمالياً جديداً يثبت خاصية النموذج المحدود لـ "الجزء المحروس" من المنطق من الدرجة الأولى مع حد علوي أمثل بأسٍ مزدوج لأس المجموعات الدنيا، والذي تم نزع العشوائية منه لاحقاً وتوسيعه ليشمل "الجزء ثلاثي الحراسة".
تقدم هذه الورقة توحيداً بسيطاً بين رتب المسارات الدلالية الرتيبة ورتب المسارات الموزونة، وتُظهر تطبيقها كرتيبات اختزال، وأزواج اختزال، ورتيبات اختزال كلي أرضي لإثبات إنهاء نظم إعادة كتابة الحدود.
تحدد هذه الورقة مشهد التعقيد الحسابي للتحقق من الشبكات العصبية ذات التغذية الأمامية في الإعدادات المكممة، حيث تثبت أن عملية التحقق تظل مسألة (NP-complete) للشبكات ذات الدقة الحسابية الثابتة تحت كل من مواصفات المتجهات الخطية ومتجهات البت، بينما توفر حدوداً عليا جديدة للشبكات المكممة ديناميكياً تحت مواصفات متجهات البت.
تقترح هذه الورقة إطار عمل استدلالي هجين حيث تقوم النماذج اللغوية الكبيرة بتوليد كود بايثون لترميز مهام الاستدلال القائمة على التفضيلات كمسائل MaxSAT، والتي يتم حلها والتحقق منها بواسطة أدوات حل دقيقة لتحقيق معدلات أعلى بكثير من حيث الجدوى والصحة مقارنة بالنماذج المرجعية التي تعتمد على الإجابة المباشرة أو سلسلة الأفكوت.
تقدم هذه الورقة مخطط التبعية Dpure القائم على المسارات النقية، والذي يُمكّن نظام الإثبات DQRAT من تحقيق التكافؤ-p مع نظام Independent Extended QU-Res القوي، ويتحقق من هذا التقدم من خلال فاحص أولي ودمجه في برنامج حل Qute.