1215 ورقة بحثية
تقدم هذه الورقة وتنفذ إطار عمل قائماً على (ASP(Q)) للاستعلام المتسامح مع عدم الاتساق للبيانات ذات الأولوية باستخدام إصلاحات مثالية من نوع "باريتو"، و"عالمية"، و"إتمامية"، مقدمةً بذلك أولى الأنظمة التي تعتمد دلالات عالمية-مثلى ومؤصلة، مع تحليل تعقيدها الحسابي وجدواها العملية.
تقترح هذه الورقة البحثية إطار عمل A-IC3، وهو إطار تعلم آلي خفيف الوزن يستخدم خوارزمية "المتعدد الأذرع" (multi-armed bandit) لاختيار استراتيجيات التعميم الاستقرائي المثلى لخوارزمية التحقق من النماذج لعتاد IC3 بشكل ديناميكي، مما يحسن أداءه وقابليته للتوسع بشكل كبير على مجموعة اختبار معيارية ضخمة.
تقدم هذه الورقة أنظمة إعادة كتابة المصطلحات المدمجة في الرسوم البيانية لتوسيع نطاق مشكلات المعرفة القابلة للتقرير في تحليل بروتوكولات الأمن، وذلك من خلال إثبات قابلية التقرر للفئة الفرعية التقاربية الانكماشية مع إثبات عدم قابلية التقرر للفئة الأوسع، إلى جانب تقديم نتائج الدمج مع النظريات المساواتية الأخرى.
تكشف هذه الدراسة أنه في حين يمكن لنماذج المحولات (transformer models) أن تتعلم بفعالية وتعمم الاتصال المتعدي على الرسوم البيانية شبيهة الشبكات منخفضة الأبعاد من خلال التوسع، إلا أنها تواجه صعوبة في القيام بذلك على الرسوم البيانية المعقدة التي تحتوي على العديد من المكونات غير المتصلة أو الهياكل عالية الأبعاد.
تقدم هذه الورقة APPL، وهو منطق موحد بأسلوب هوار (Hoare-style) يرتكز على إطار دلالي مرن يستوعب المنطق القياسي، ومنطق عدم الصحة، والمنطق الفائق، مع توفير أنظمة برهان سليمة ومكتملة نسبيًا لخصائص البرامج الملموسة والمجردة على حد سواء.
تقدم هذه الورقة إطار عمل جديداً لتوليد الترتيب يعتمد على حل مشكلات القابلية للإرضاء (SAT) ويدمج التسمية القانونية العودية مع خوارزمية NAUTY للتغلب على قيود القابلية للتوسع السابقة، مما يتيح أول تعداد شامل لمجموعات كوشين-سبيكر الصغيرة في البعد 3، ويتحقق من أن مجموعة شوتيه المكونة من 33 شعاعاً هي الأصغر التي تحتوي على مجموعة سياقية مستقلة عن الحالة المكونة من 25 شعاعاً كاملة.
تقدم هذه الورقة الموسعة نموذجاً رسمياً لتصور شهود (witnesses) ومثبتات كذب (counterexamples) منطق التوقيت الحسابي (CTL) على نماذج ذات حالة صريحة لتعزيز الفهم البشري، مع تقديم توصيفات للأدلة الدنيا لكل عامل زمني وتنفيذ ملموس، جنباً إلى جنب مع براهين لجميع النتائج.
تؤسس هذه الورقة عائلة من ثنائيات نوع "ستون" (Stone-type dualities) بين الجبرات الجهوية (modal algebras) والفضاءات العلاقاتية، مبيّنةً كيف تؤثر تعريفات المورفيزمات المتنوعة على بناء النقاط، وكيف تعمل العلاقات شبه المستمرة على تبسيط التناظر بين البديهيات الجهوية والخصائص العلاقاتية.
توضح هذه الورقة مبادرة جارية لتطوير إطار عمل ومكتبة لـ Isabelle/HOL من أجل التحقق الرسمي من تحليل خوارزميات الثنائية الأولية (primal-dual)، مع استعراض تطبيق ذلك من خلال الصياغة الرسمية لكل من خوارزميات المطابقة الكلاسيكية مثل الطريقة المجرية (Hungarian Method) والنهج الحديثة مثل خوارزمية أدوريدز (Adwords algorithm).
تثبت هذه الورقة أن شروط التعقيد دقيق التفاصيل للوصول المباشر إلى إجابات الاستعلام التلازمي، والمعروفة سابقاً لقواعد البيانات غير الموسومة، تمتد لتشمل الاستعلامات ذات التجميعات والوسوم الحلقية (بشرط استبعاد الوسم من الترتيب)، مع اشتقاق أيضاً شروط جدوى جديدة لتجميع العدّ-المتميز وتحليل تأثير تضمين القيم المجمعة في الترتيب أو استخدام خصائص حلقية محددة.