1215 ورقة بحثية
تثبت هذه الورقة أن مختلف الدوال ذات النهاية (finitary endofunctors) عبر فئات متنوعة —بما في ذلك المجموعات، والمجموعات المرتبة جزئياً، والفضاءات المتجهة، والرسوم البيانية، والفضاءات الطوبولوجية— تمتلك كوجليات طرفية (terminal coalgebras) يمكن بناؤها كحدود معدودة لسلاسل الكوجليات الطرفية الخاصة بها، مما يوسع ويثبت النتائج التي اقترحها ووريل (Worrell) في الأصل.
تؤسس هذه الورقة إطاراً كوجبرياً للمنطقيات الديناميكية متعددة القيم يدمج القضايا ذات القيم والأنظمة الموزونة، حيث تثبت أن العمليات الكوجبرية القابلة للاختزال تحافظ على التماثل الجزئي وتؤدي إلى نتائج اكتمال قوي عام لمنطق PDL الخالي من التكرار ومنطق اللعبة فوق السلاسل المتناهية ومنطق لوكاسيفيتش.
تقدم هذه الورقة تقنية لترجمة الجزء المتزامن من منطق سيجنال الزمني (SSTL) إلى مراقبين متزامنين نمطيين ضمن لغة Lustre، مما يتيح التحقق من الأنظمة السيبرانية الفيزيائية في وقت التشغيل والتحقق الاستاتيكي مع دعم التعشيب التعسفي للخصائص المحدودة وعامل خارجي غير محدود عالمياً للمراقبة عبر الإنترنت.
تقدم هذه الورقة خوارزميات عالمية ومحلية مرنة لحل نظم المعادلات عبر المجموعات الجزئية المرتبة النويثرية (Noetherian posets) من خلال استخدام أوراكل اعتماد (dependency oracles) قابل للتخصيص لتوجيه الاستكشاف وضمان الإنهاء السليم، محققةً أداءً تنافسياً مع السماح بمقايضات مبدئية بين الدقة والكفاءة.
تقدم هذه الورقة إطار عمل استنتاجيًا على مستوى البرنامج لتوليف الاستراتيجية متعددة الأهداف في البرامج الاحتمالية ذات عدم التحديد، وذلك باستخدام محول توقعات مسبقة متعدد الأهداف يربط التوقعات اللاحقة بمجموعات القيم القابلة للتحقيق ضمن مجال "هوار" (Hoare) القدري المحدب للتعامل بشكل سليم مع عمليات ماركوف لقرار (MDPs) ذات الحالات غير المحدودة دون اشتراط وجود فضاءات حالات منتهية.
يقدم CAPRI سير عمل لإصلاح البراهث مدركاً للعقود لـ Isabelle يستفيد من النماذج اللغوية الكبيرة لإصلاح البراهث الفاشلة مع فرض عقود تحرير صارمة لضمان قيام المطورين فقط بالتغييرات المصرح بها، مما يظهر معدلات نجاح عالية في الإصلاح دون المساس بسلامة الكود في التقييمات التجريبية.
تقدم هذه الورقة "منطق المجموعات الخطية المنفصلة" (Discrete Linear Ensemble Logic)، وهو صياغة معرفية للمجال الحيوي الطبي تجمع بين الأنماط الزمنية والمكانية والقياسية، وتؤسس نظريته الجوهرية من خلال إثبات أن قابلية إرضائه هي -complete، وأن تعبيره يتجاوز بصرامة اللغات -star-free بينما لا يقارن باللغات -regular، وأن قابليته للتقرير تعتمد على تضمينه في حساب بريسر المونادي (monadic Presburger arithmetic).
تقدم هذه الورقة مورفيزمات هيكلية وعوامل منطقية للشروط المتداخلة المستخدمة في تحويل الرسوم البيانية، مع إثبات اتساقها مع الاستلزام المنطقي وتأطير هذه النتائج ضمن سياق فئوي لإثبات خصائص التبعية والشمولية.
تقدم هذه الورقة خوارزمية تقرر ما إذا كانت لغة الدفع المرئي (visibly pushdown language) تنتمي إلى فئة التعقيد من خلال إما تأكيد عضويتها، أو إثبات أنها صعبة بالنسبة لـ ، أو اختزالها إلى فئة فرعية محددة من لغات الدفع المرئي (VPLs) ذات التعقيد المتوسط التي لا يزال وضعها التعقيدي فرضية مفتوحة.
تقدم هذه الورقة برهاناً بنائياً على امتلاك منطق الديناميات القضايا (PDL) لخاصية استكمال كرايغ، وذلك عبر توظيف نظام جدول (tableau) دوري مع آلية تحميل وطريقة "مايارا" معدلة لحساب المستكملات، مما يحل مشكلة مفتوحة منذ زمن طويل بعد أن تم سحب أو انتقاد محاولات سابقة.