1215 ورقة بحثية
تقترح هذه الورقة نهج تحقق هجين يدمج بين دلالات الخطوة الصغيرة (small-step) والدلالات الكلية (big-step) عبر واجهة تجريدية مشتركة لتمكين التحقق الرسمي من تحسينات الحلقات الهيكلية، مثل بسط الحلقة الكامل (full loop unrolling)، ضمن مسار مترجم CompCert مع الحفاظ على جميع الضمانات الدلالية العليا.
تقترح هذه الورقة إطار عمل لدلالات دلالية (denotational semantics) يتيح كشف تعارض ثلاثي القيم سليم لسياسات ODRL عبر قواعد معرفية غير متجانسة من خلال رسم خرائط القيود لمفاهيم قواعد المعرفة، مع إثبات أن التعارضات تظل محفوظة تحت عملية المحاذاة مع التدهور التدريجي للقيم المجهولة، والتحقق من صحة النهج باستخدام 154 معياراً عبر تصنيفات ومجالات هيكلية متنوعة.
تقدم هذه الورقة تصنيفاً جديداً لألعاب "الطالب-المعلم" (Student-Teacher Games) بناءً على الجولات والاستعلامات لفصل الفئات الفرعية من الهرم متعدد الحدود ونظريات الحساب المحدود المقابلة لها تحت فرضية عدم انهيار الهرم، مما يؤدي إلى حل مشكلات مفتوحة تتعلق بالجمع المحدود والاستقراء مزدوج الطول، مع توسيع نتائج عدم القابلية للإثبات المتعلقة بحدود الدوائر المنطقية.
يقدم هذا البحث نظام noDice، وهو نظام يوسع محرك الاستدلال الاحتمالي المنفصل Dice لدعم عدم الحتمية من خلال بناء عمليات ماركوف لاتخاذ القرار واستخدام مخططات القرار لاستنتاج التوزيعات على المجدولين بكفاءة في البرامج الخالية من الحلقات.
تقدم هذه الورقة VSCAN، وهو إطار عمل للتحقق الرسمي يضمن متانة أنظمة الاتصال الدلالي القائمة على الشبكات العصبية العميقة ضد الضجيج التنافسي التوليدي، وذلك عبر ترميز قيود واقعية في البرمجة الخطية المختلطة، مما يكشف عن نقاط الضعف ويظهر مقايضة بين الأمن والكفاءة في أبعاد الفضاء الكامن.
تضع هذه الورقة نظرية ثنائية لمشكلات التشاكل المتعلقة بالبنى الآلية، حيث تثبت أن هذه المشكلات إما أن تكون قابلة للتقرير في فضاء لوغاريتمي غير حتمي (NL) أو غير قابلة للتقرير، مع توصيف دقيق للقابلية للتقرير من خلال كون البنية المستهدفة ذات ثنائية منتهية (أو بالتكافؤ، كونها قابلة للتعريف في المنطق من الدرجة الأولى)، وهي نتيجة تسري على كل من التشاكلات القياسية والمنتظمة.
تقدم هذه الورقة أول دراسة شاملة لتراتيب الصقل لكل من البرامج الكمومية الحتمية وغير الحتمية، حيث تُثبت وجود تقابلات دقيقة بين مختلف فئات المحمولات الكمومية (المساقط، والمؤثرات، ومجموعات المؤثرات) والتراتيب الرياضية أو التراتيب النظرية للمجال القياسية تحت معايير الصحة الكلية والجزئية.
تقدم هذه الورقة نسخة كوجبرية معممة لتمهيدية كونيغ (König's lemma) على التوابع النهائية المحدودة (finitary endofunctors) فوق الفئات محلياً المحددة نهائياً (locally finitely presentable categories)، حيث تُثبت أن الكوجبرات جيدة التأسيس (well-founded coalgebras) هي تجمعات موجهة (directed joins) لجوهرها الكوجبري المولد نهائياً، وتستفيد من هذه النتيجة لتقديم إنشاءات وبراهين جديدة للجبرات الأولية (initial algebras).
تقدم هذه الورقة مجموعة من الخوارزميات الآلية للتفسير الميكانيكي التي تستفيد من التحقق من الشبكات العصبية لاكتشاف دوائر ذات ضمانات مثبتة فيما يتعلق بمتانة نطاق المدخلات، والترقيع المتين، والحد الأدنى، مع الكشف عن روابط نظرية جديدة بين هذه الخصائص وإثبات أدائها المتفوق على نماذج الرؤية مقارنة بالطرق الاستدلالية القياسية.
تقدم هذه الورقة نظرية النوع الملتوي (TTT)، وهي نظرية نوع موجهة جديدة تتميز بعملية "التواء" مبتكرة ودلالاتها عبر التعيينات المعتمدة ثنائية الجوانب، مما يتيح الاستدلال بأسلوب نظرية النوع الهوبفية (HoTT) حول الفئات ويقدم برهاناً تركيبياً لتمهيدية يوندا.