1215 ورقة بحثية
تقدم هذه الورقة إطاراً عاماً لإعادة الكتابة الاستقرائية المشتركة (coinductive rewriting) للكائنات اللانهائية، وتُعرّف مفهوم "الضغط" (compression) —وهو القدرة على اختزال تسلسلات إعادة الكتابة العابرة للأعداد الترتيبية إلى طول — مع تطبيق هذه النتيجة لإثبات أن حذف القطع (cut-elimination) في نظام الإثبات غير الجيد هو عملية قابلة للضغط.
تقترح الورقة البحثية GORED، وهو حلّال أمثلة عام يعزز من تنوع حل المشكلات عبر تقليص مشكلات الأمثلة المتنوعة تلقائياً إلى نماذج MaxSAT، مما يسمح لإطار عمل موحد واحد بتحقيق جودة حل تضاهي الخوارزميات المتخصصة.
تقدم هذه الورقة منطقاً احتمالياً ضبابياً () لصياغة ودراسة تعقيد "الاستدلال الاحتمالي"، وهي عملية إيجاد توزيعات احتمالية أو عبارات تستلزم منطقياً معطيات معينة بناءً على ملاحظات حول احتمالات الأحداث.
يعتبر Reelay إطار عمل موحداً وعالي الأداء لمراقبة المنطق الزمني عبر الإنترنت، يقوم بترجمة المواصفات الصورية المتنوعة (مثل LTL وMTL وSTL) إلى رسوم بيانية حسابية لتدفق البيانات المتزامن عالية الكفاءة، مما يتيح التحقق في وقت التشغيل للأنظمة السيبرانية الفيزيائية عبر مختلف المنصات العتادية.
تقدم هذه الورقة وتُحلل منطقاً جهاتياً ضبابياً صُمم لنمذجة الاستدلال الاحتمالي المتعلق بالأفعال والمعرفة، مما يوفر إطاراً دلالياً قائماً على أطر كريبكي ويحدد التعقيد الحسابي لمشكلات القابلية للإرضاء الخاصة به.
تتقصى هذه الورقة وتُوصّف فئات الرسوم البيانية التي تقبل فيها مسألة التحقق من النموذج من الدرجة الأولى خوارزمية زمن ثابت المعلم (FPT) عندما تكون مُعلمة بعدد المتغيرات في الصيغة، وتحديداً من خلال تقديم توصيفات في السياقين الرتيب والمتوارث.
يُعد DEKL 2.0 إطار عمل نظري للأنواع المعتمدة يوحد بين الآثار التنفيذية ومراجعة المعرفة من خلال نمذجة المعرفة كـ "presheaf" فوق فئة أثر (trace category)، مما يسمح للتطور غير الرتيب بالظهور دلاليًا مع الحفاظ على حساب برهان رتيب.
تثبت هذه الورقة أن مشكلة وجود الخطة في المنطق المعرفي غير قابلة للتقرير، حتى في ظل ظروف مقيدة للغاية مثل العمق الموجه المحدود لمتطلبات الأفعال وغياب الشروط اللاحقة.
تتناول هذه الورقة التباعد الدلالي بين لغتي المخططات الشاملة (ShEx) و(SHACL) العودية من خلال تقديم إطار رسمي موحد يوضح العلاقات بين دلالات النقطة الثابتة الدنيا والنقطة الثابتة العليا، ويثبت وجود أجزاء متكافئة تعبيرياً بين المعيارين، ويحلل التعقيدات الحسابية الخاصة بكل منهما.
تقدم هذه الورقة البحثية VerCors-relaxed، وهو امتداد لأداة التحقق الاستنتاجي VerCors التي تقوم بترميز التزامن في الذاكرة الضعيفة باستخدام بروتوكولات قائمة على الرؤية ومنطق الفصل القائم على الأذونات لتمكين التحقق الآلي من البرامج المتزامنة التي كانت تقتصر سابقاً على البراهين اليدوية.