1215 ورقة بحثية
تحاول هذه الورقة إحياء مبدأ تشايتين الاستدلالي لوزن النظريات مع إثبات أن ثابت تشايتين أوميغا ليس احتمال توقف تحت أي مقياس منفصل لانهائي، ومن ثم تقترح طرقاً بديلة لتعريف احتمالات التوقف.
تقدم هذه الورقة نظام إثبات استنتاجي سليم وكامل يعتمد على التماثل النسبي والاستدلال التعاوني لتمكين التحقق التفاعلي والنمطي من استيفاء عقود الأجهزة والبرمجيات، كما تم توضيحه من خلال صياغته الرسمية في مساعد الإثبات Rocq وتطبيقه على براهين أمنية معقدة.
تُبين هذه الورقة أنه من خلال الانتقال من التركيب الكارتيزي التقليدي إلى إطار مونويدي دياغرامي، يمكن تحقيق أكسيوماتية كاملة لحساب العلاقات الكامل —متجاوزةً نظريات الاستحالة السابقة— عبر تقديم "حساب العلاقات النيو-بيرسية"، الذي يجمع بين الفئات الثنائية الكارتيزية والخطية للوصول إلى القدرة التعبيرية للمنطق من الدرجة الأولى.
تقدم هذه الورقة نهجاً للتكيف في التحكم للأنظمة ذاتية القيادة يعمل على توسيع قدراتها التشغيلية ديناميكياً للتعامل مع سيناريوهات خارج نطاق التصميم التشغيلي (out-of-ODD)، مع توفير ضمانات كمية رسمية في الوقت ذاته لضمان الأداء الموثوق في ظل الظروف غير المتوقعة.
تقدم هذه الورقة نهجاً قائماً على حل مشكلات التماثل (SMT) لاستنتاج النماذج البيولوجية باستخدام دوال غير مفسرة مع قيود الرتابة، وتثبت من خلال اختبارات قياسية مكثفة أن استراتيجية التجسيد الكسول الخاصة بها تتفوق بشكل كبير على كل من الترميزات المكممة الساذجة والأدوات المتطورة المتخصصة في هذا المجال مثل Bonesis وAEON.
تقدم هذه الورقة دلالات صورية موحدة للتعبيرات الحاملة للقياس تتبع المصدر والتعريف لإرساء أحكام إعادة الكتابة أحادية الاتجاه والتبادلية، مبرهنةً على أن التساوي الجبري العادي يفشل كأصل لإعادة الكتابة بسبب مشكلات مثل إعادة استخدام الملاحظة واختلافات النطاق الناجمة عن القسمة، مع صياغة جميع النتائج رسمياً في لغة Lean 4.
تقدم هذه الورقة المفهوم الرسمي لـ "التفكيكية العصبية" القائم على الحفاظ الدلالي عند حدود القرار، وتقترح إطار عمل SAVED لتقييم وتحقيق التفكيك النموذجي تجريبياً، كاشفةً أنه في حين تدعم نماذج المحولات اللغوية (Transformers) هذا النوع من التفكيك بشكل كبير، فإن النماذج الرؤيوية غالباً ما تظهر قيوداً جوهرية.
تقدم هذه الورقة إطاراً معلماً من إعادة الترتيب ذي الشرائح- يجسّر الفجوة بين المراقبة القائمة على التبادلية (commutativity) التي تتسم بالكفاءة ولكنها محدودة، وبين تكافؤ "القراءة من" (reads-from) المستعصي، مما يتيح المراقبة التنبؤية ذات المساحة الثابتة للمواصفات المنتظمة مع المقايضة المنهجية بين القدرة التعبيرية والتكلفة الحسابية.
تقدم هذه الورقة تنفيذًا أوليًا في برنامج التحقق VerCors يدعم الأنواع الفرعية للمحمولات (predicate subtypes) لتحديد قيود نطاق المتغيرات، ويتميز بالتوليد التلقائي للمواصفات، والقدرة على دمج أنواع فرعية متعددة، ووضع التشغيل الصارم لتعزيز فحص تجاوز السعة.
تقترح هذه الورقة إطار عمل جديداً من النوع العالمي يوسع أنواع الجلسات متعددة الأطراف عبر دمج دلالات الفشل الصريحة والمشاركة الديناميكية لضمان سلامة الاتصال وحيويته رسمياً في تطبيقات الويب عالية التزامن والمقاومة للأعطال.