1215 ورقة بحثية
تقدم هذه الورقة Kofola، وهي أداة فعالة ومتينة توظف إطار عمل معياري لتفكيك أوتوماتا بوشي (Büchi automata) إلى مكونات متصلة بقوة من أجل مواءمة التحقق من الاستكمال والاحتواء، مما يظهر أداءً فائقاً على الأدوات الرائدة حالياً من خلال التحقق من الفراغ أثناء التشغيل واستخدام خوارزميات استدلالية جديدة.
تتناول هذه الورقة نقص دراسات القياس المنهجية على نماذج (SAT) الصناعية من خلال تحليل معيار مرجعي ضخم لـ (BMC)، حيث تُثبت أن معامل "proofdoor" المقترح حديثاً —والذي يمثل تسلسلاً من المستنبطات— يفسر بنجاح قابلية توسع أداء الحلول حيث تفشل المعاملات الهيكلية التقليدية.
تؤسس هذه الورقة إطاراً كوجلياً (coalgebraic) لأنظمة الإثبات غير جيدة التأسيس، والتي تُوصّف شرط الأثر العالمي (GTC) عبر الكوجليات العودية، وبذلك توفر صياغة فئوية للسلامة باعتبارها وجود مورفيزمات (morphisms) فريدة من الكوجلي إلى الجبري.
تقدم هذه الورقة ركائز المخطط البياني للأحداث الحتمية، وهي نموذج عالمي شفاف وغير معلمي يمثل الحالة كسجلات ثلاثية (RDF) مضافة فقط، ويُمكّن من الاستدلال المضاد للواقع بدقة من خلال تفرع السجل، مما يُظهر أداءً فائقاً على كل من الأوراكل الرمزية ونماذج اللغات الكبيرة المعلمية في معايير CLEVRER وtwin-EventLog.
تقترح هذه الورقة إطار عمل رمزيًا يحول السرديات غير المهيكلة لإنفاذ القانون إلى حقائق مرتبطة بالأدلة ورسوم بيانية زمنية من خلال دمج التحليل الدلالي، ورسم خرائط الأنطولوجيا، والاستنتاج، مما يظهر دقة عالية في استخراج تفاصيل الحوادث الرئيسية من تقارير جرائم الممتلكات.
تقدم هذه الورقة LeanBET، وهو مسار تحليل مساحة سطح بروناور-إيميت-تيلير (BET) قابل للتنفيذ بالكامل ومتحقق منه رسميًا تم تنفيذه بلغة Lean 4، والذي يضمن الصحة الرياضية مع تحقيق توافق عددي شبه مثالي مع التنفيذ المرجعي BETSI الراسخ.
تقترح هذه الورقة إطار عمل هجين يجمع بين الأساليب الصورية (تحديداً منطق الزمن الخطي) والتعلم الآلي لتمكين التدقيق الفعال دون اتصال بالإنترنت والمراقبة في وقت التشغيل لأنظمة الذكاء الاصطناًعي ذات الصندوق الأسود، مما يثبت أن هذه التقنيات تتفوق على النماذج المرجعية للنماذج اللغوية الكبيرة في اكتشاف انتهاكات القيود الزمنية ويمكنها التخفيف من المخاطر بنشاط مع الحفاظ على أداء المهام.
تقدم هذه الورقة الهندسة الجبرية الرسومية (GAG)، وهي إطار عمل رسومي شامل وكامل للجبر التبادلي والمتنوعات الأفينية، توحد دراسة شبكات القيود متعددة الحدود وحساب ZH للـ qudit للحوسبة الكمومية.
تقدم هذه الورقة "منطق السلسلة الخطية" (LCL)، وهو إطار عمل للمنطق المكاني يستفيد من الربط بين حالات ضرب المصفوفات الدورية والخرائط الموجبة تماماً لتمكين التحقق التقريبي القابل للتوسع من الخصائص المعتمدة على الحجم والخصائص التقاربية في الأنظمة الكمومية متعددة الأجسام أحادية البعد.
تقدم هذه الورقة شبكات الإثبات لـ PiL، وهو امتداد للمنطق الخطي متعدد الإضافات من الدرجة الأولى يتيح ترميزاً ضحلاً لعمليات حساب π (pi-calculus)، وتثبت صحتها، وقابليتها للتسلسل، وقدرتها على تمثيل اشتقاقات حساب التتابعات بشكل معياري بالنسبة لتبديلات القواعد.