1215 ورقة بحثية
تؤسس هذه الورقة إطاراً برهانيّاً للاستدلال البايزي عبر رسم خرائط لشبكات بايز إلى شبكات برهانية منطقية خطية، بهدف توفير طرق رسومية تركيبية توازن بين المرونة الهيكلية والكفاءة الحسابية.
تقدم الورقة البحثية CSLib، وهو إطار عمل مفتوح المصدر مصمم لإنشاء قاعدة معرفية شاملة لعلوم الحاسوب داخل مساعد الإثبات Lean على غرار Mathlib، مما يتيح اعتماداً تعليمياً أوسع وييسر تطوير أنظمة واسعة النطاق موثقة رسمياً.
تقدم هذه الورقة Cargo Sherlock، وهو إطار عمل قائم على تقنية التحقق من النماذج المعتمدة على التقييد (SMT)، يعمل على قياس موثوقية البرمجيات من خلال الجمع رسمياً بين العوامل البشرية القائمة على البيانات الوصفية وتحليل الكود للكشف عن هجمات سلاسل التوريد في تبعات لغة رست (Rust).
تقدم هذه الورقة ، وهي حساب لامتدا خطي كلاسيكي جديد يعتمد على التناقض (contraposition) وآلية "تعويض تناقضي" فريدة، والتي ثبت أنها سليمة، وكاملة، وذات تطبيع قوي لمنطق الخطية الأسي المتعدد (MELL) الكلاسيكي.
توسع هذه الورقة شرط التدرج الضعيف لـ "تيو" الخاص بمنطق التعريفات ليشمل التكميم العام (نابلا) والاستقراء العام، مما يمكّن مساعد الإثبات "أبيلا" من دعم التعريفات التي تتضمن حدوثات سالبة، مثل تلك المطلوبة في العلاقات المنطقية.
تقدم هذه الورقة طريقة جديدة للتحقق الرمزي من نماذج شبكات بيتري تستخدم الفترات المعممة على المتجهات للتغلب على انفجار مساحة الحالة، مظهرةً أداءً واعداً في مهام التحقق من منطق التوقيت الحسابي (CTL) العالمي من خلال تقنيات التشبع والتجميع الفعالة.
تقدم هذه الورقة أول صياغة رسمية في Isabelle/HOL لصحة وخوارزمية أورلينن (Orlin) لزيادة السعة (capacity scaling) من حيث وقت التشغيل في الحالة الأسوأ لتدفقات التكلفة الأدنى، بما في ذلك تنفيذ قابل للتنفيذ بالكامل مشتق عبر صقل تدريجي واختزال مُتحقق منه من المسألة العامة.
تقدم هذه الورقة إطار عمل للتحقق الرسمي المخصص الذي يدمج بيانات الاستشعار مع السياق الفردي لنمذجة والتحقق رسمياً من أنشطة الحياة اليومية لكبار السن الذين يعيشون بشكل مستقل، باستخدام المنطق الزمني الخطي للكشف عن انتهاكات السلامة وتوليد أمثلة مضادة تفسيرية.
تستكشف هذه الورقة تطبيق المنطق من الدرجة الأولى مع الجمع (FO(SUM)) وامتداده التكراري (IFP(SUM)) كلغات استعلام للشبكات العصبية الممثلة كرسوم بيانية موزونة، مع تقديم أمثلة توضيحية وتحليل قدرتها التعبيرية وتعقيدها الحسابي.