1215 ورقة بحثية
تقدم هذه الورقة دلالات جبرية ميكانيكية للتنفيذ المحكوم، تم صياغتها في ٣٢ وحدة من وحدات روك (Rocq) باستخدام أشجار التفاعل والاستقراء المشترك، مما يؤسس لفئة متناظرة مونويدية حيث يتم وضع قواعد الحوكمة كبديهيات، وتكون تركيبية ومتزامنة مع القدرة على التعبير، مما يضمن أن جميع البرامج القابلة للإنشاء محكومة مع الحفاظ على اكتمال تورينج واستبعاد الإدخال والإخراج غير الوسيط.
تتناول هذه الورقة البحثية محدودية التعظيم الجشع لدالة Q في مهام المنطق الزمني ذات الأفق اللانهائي غير المخصوم عبر بناء سياسات غير ماركوفية تعتمد على تاريخ الحالة لضمان المثالية للمواصفات المتداخلة، وتوضيح كيف يمكن لدوال Q أن تعمل كمرشحات سلامة لمتطلبات المنطق الزمني المعقدة.
تتناول هذه الورقة مشكلة الاستنباط من نوع ABox لقواعد المعرفة غير المتسقة عبر تعريف مفاهيم مناسبة للاستنباط تحت دلالات الإصلاح، وتقديم تحليل شامل للتعقيد لمنطق الوصف خفيف الوزن DL-Lite وEL_bot.
تتناول هذه الورقة تحدي مقارنة لغات توصيف الأحداث المتباينة من خلال رسم خرائط لها نحو إطار عمل موحد لـ "داتالوك الزمني" (Temporal Datalog)، وتقديم "رسوم بيانية للمحفزات المتدفقة" (Streaming Trigger Graphs) لتمكين التعرف على الأحداث المركبة بكفاءة وقابلية للتعميم عبر تدفقات البيانات عالية السرعة.
تتقصى هذه الورقة مدى قابلية التقرير لعملية احتواء مستندات SHACL، حيث تثبت أن المشكلة غير قابلة للتقرير تحت دلالات النموذج المدعوم والمستقر، ولكنها قابلة للتقرير في زمن أسي أحادي تحت دلالات النموذج المرتكز على الأسس عبر ترجمة مبتكرة إلى حساب ميو الهجين.
تقدم هذه الورقة "جبر البناءات التكرارية" (AIC)، وهو إطار جبري بحت للاستدلال حول تكرارات النقطة الثابتة على الشبكات الكاملة، مما يتيح الإثبات الآلي للنظريات، ويعمم النتائج القائمة مثل مبدأ "تارسكي-كانتوروفيتش"، ويحدد الحدود النظرية لترسيمه الأكسيومي الخاص.
تقدم الورقة البحثية iSMC، وهو أول مدقق نماذج رمزي يعتمد على مخططات القرار ثنائية التعيين (BDD) وذاتي التصديق لمنطق شجرة الحوسبة (CTL) مع متطلبات العدالة، والذي يضمن صحة إجاباته من خلال إجراء تصديق تفاعلي مقتبس من تقنية حل مسألة الوجود الكلي الكمي (QBF).
تقدم هذه الورقة وتُعرف فئة جديدة من عمليات تحويل الأشجار (tree transductions)، المعرفة بآلات هيني (Hennie machines) التي تسير على الأشجار مع زيادة خطية في الحجم بالنسبة للارتفاع، والتي توسع دوال الأشجار المنتظمة توسعاً صارماً، ويُبين أنها مغلقة تحت تركيبات محددة ومعادلة لحساب لامدا الخطي مع الصفوف (tuples) الجمعية.
تقترح هذه الورقة إطار عمل هجين لحل مشكلات الـ SAT يستفيد من أجهزة أخذ عينات "إيسينج" ذات البتات الاحتمالية لتوجيه تعلم العبارات المدفوع بالصراع (CDCL) باستخدام افتراضات عالية الاتفاق، مما يحقق تخفيضات كبيرة في جهد البحث في معايير محددة لـ 3-SAT مع استخدام بوابات تعلم آلي لتحديد متى يكون هذا التوجيه مفيداً.
تقدم هذه الورقة إجراءً لاتخاذ القرار للمنطق ، الذي يوسع نظرية المجموعات المحدودة بفترات صحيحة محدودة تسمح بمتغيرات غير مقيدة، وتبرهن على فائدته العملية من خلال أداة في التحقق التلقائي من ليمات الثبات لخوارزمية مصعد.