1215 ورقة بحثية
تثبت هذه الورقة أن المنطق من الدرجة الأولى فوق الأشجار اللانهائية يتم استيعابه بدقة بواسطة فئتين من أوتوماتا الأشجار المترددة المقابلة لـ \PolPCTL و \CTLsf، مما يوفر توصيفاً موحداً قائماً على الأوتوماتا ويكشف أن القابلية للتعريف من الدرجة الأولى تقتصر جوهرياً على خصائص السلامة أو السلامة المشتركة (co-safety) على طول كل فرع.
تقدم هذه الورقة نهجاً جديداً قائماً على القوالب لتوليد فرضيات الاستقراء تلقائياً ضمن الاستقراء بإعادة الكتابة المحدودة لأنظمة إعادة الكتابة المقيدة منطقياً من الرتبة العليا، مما يُمكّن من إثبات تكافؤات البرامج التي لم يكن من الممكن الوصول إليها سابقاً عبر التعرف على البنى البرمجية النمطية كحالات دالة من الرتبة العليا.
تقدم هذه الورقة البحثية مِحلاً جديداً لـ SMT يعتمد على خوارزمية DPLL() يقوم بتنسيق وحدات متعددة لتقرير قابلية إشباع المعادلات متعددة الحدود فوق الحقول الأولية بكفاءة، مما يظهر أداءً فائقاً في التحقق من بروتوكولات إثبات المعرفة الصفرية مقارنة بالأدوات الحالية المتطورة.
تتقصى هذه الورقة التعقيد الحسابي لعمليات ماركوف لاتخاذ القرار المتينة ذات مجموعات عدم اليقين متعددة الأوجه، حيث تثبت أن مسألة العتبة تقع ضمن فئة NP في حالات المستطيلات (s,a)، وفي فئة PSPACE في حالات المستطيلات s، بينما تثبت أن حلها في وقت حدودي من شأنه أن يحسم المسألة المفتوحة منذ زمن طويل حول ما إذا كانت ألعاب التكافؤ تقع ضمن فئة P.
تقدم هذه الملاحظات المحاضرية الأسس القائمة على نظرية الأوتوماتا، والمنطق الزمني، والمعرفة، للتحقق من وقت التشغيل، حيث تغطي صياغات المواصفات، والتشخيص، والعتامة، وقابلية المراقبة لشرح كيفية بناء التحليل غير المتصل للمراقبين للأنظمة ذات الرؤية الجزئية، مع معالجة تحديات الامتدادات الزمنية في البيئات الزمنية الحقيقية.
تثبت هذه الورقة أن جميع العائلات المنطقية للمتجهات المتقدمة (profunctors) المستقرة والكلية في نموذج علاقي ذي صلة بالبراهين قائم على الزمر (groupoids) يمكن تعريفها بالكامل بواسطة شبكات البراهين (proof-nets) للمنطق الخطي الضربِي مع قاعدة MIX، مما يبرهن على أن الاستقرار يعمل كمعيار صحة حاسم لهذا التوصيف.
تقترح هذه الورقة نظام استنباطي لانهائي، AA*، لمنطق معرفي غير متزامن يأخذ في الحسبان السجلات التعسفية لإرسال واستقبال الرسائل، مما يعمم الأعمال السابقة عبر التخلي عن نهج نظام الاختزال وافتراض عدم استلام أي رسائل.
تقدم هذه الورقة صياغة لبناء أعداد كوشي الحقيقية القائم على نظرية النوع النوعية المتجانسة (Homotopy Type Theory) في لغة Cubical Agda، مظهرةً أن هذا النهج يتجنب مشكلات الاختيار القابل للعد، والأعباء الإضافية للـ setoid، وتتبع مستويات الكون المتأصلة في التعريفات البنائية الأخرى، مع القدرة على التحقق من صحة النوع دون الحاجة إلى مسلمات.
تقدم هذه الورقة البحثية "منطق المسارات الضبابية" (Logic of Fuzzy Paths)، وهو منطق زمني جديد لتخطيط الحركة يعامل المسارات ككيانات أساسية لفصل الهندسة عن المنطق، مما يوفر مواصفات أكثر بديهية للمستخدمين البشريين وقدرات محسنة للتعلم من العروض التوضيحية مقارنة بالأطر الحالية مثل "المنطق الزمني الإشاري" (Signal Temporal Logic).
تُبين هذه الورقة أن شرط قابلية القياس من نوع بوريل (Borel measurability) لـ "القيم العليا للفجوة الشبحية" (ghost-gap suprema) في إثبات التناظر القياسي لتعلم VC هو أقوى مما هو ضروري، حيث تُظهر بدلاً من ذلك أن الأحداث السيئة ذات الصلة هي أحداث تحليلية (analytic) وبالتالي فهي قابلة للقياس في إتمام أي مقياس بوريل منتهي، وهي نتيجة تمت صياغتها رسمياً في لغة Lean 4 بما يضعف فرضيات قابلية القياس اللازمة لإثبات قابلية التعلم بنظام PAC.