1215 ورقة بحثية
تقدم هذه الورقة "تفكيك الإثبات الاستقرائي"، وهي منهجية تفاعلية توجه المبرهنين البشريين في بناء براهين السلامة للبروتوكولات الموزعة المعقدة عبر بناء رسم بياني للإثبات الاستقرائي بشكل تدريجي، وتحديد الأمثلة المضادة محلياً، وتقطيع الحالات غير ذات الصلة للتغلب على قيود أدوات التحقق المؤتمتة بالكامل.
تثبت هذه الورقة أن الحيوية الهيكلية لشبكات بيتري المحافظة هي (EXPSPACE-complete) من خلال إثبات أن العلامات الحية الدنيا للشبكات المحافظة ذات الحيوية الهيكلية محدودة بدالة أسية مزدوجة لحجم الشبكة.
تقدم هذه الورقة إطاراً للمنطق الإبستيمي القائم على النماذج الموزونة، والذي يستخدم مقياس "المهارات الإبستيمية" لنمذجة اكتساب المعرفة ديناميكياً كعملية رفع كفاءة، والنسيان كعملية خفض كفاءة، مع تحليل المعرفة الجماعية، والقابلية للمعرفة، والقابلية للنسيان، والتعقيد الحسابي للنظام.
تقدم هذه الورقة صياغة شجرة بروهات-تيتس في مبرهن نظرية "لين" (Lean) وتُظهر فائدتها من خلال التحقق من نتيجة تتعلق بالسلاسل المتوافقة (harmonic cochains) على الشجرة.
تقدم هذه الورقة TREBL، وهو منطق زمني نسبي كامل لـ Event-B يعبر عن خصائص الحيوية عبر مسارات الحالة، ويحدد قواعد اشتقاق سليمة له، ويثبت أن الاستلزامات الصالحة يمكن اشتقاقها دائمًا في حال وجود آلات مصقولة بما يكفي حيث تكون حدود المتغيرات (variant terms) محددة بدقة.
تحدد هذه الورقة وتُوصّف ظاهرة "قصر النظر الناجم عن الأداة" (TIM)، وهي ظاهرة تحقق فيها النماذج اللغوية المعززة بالأدوات (TaLMs) دقة أعلى في الإجابات النهائية للمسائل الرياضية، ولكنها تعاني من تدهور في تماسك الاستدلال عبر معاملة مخرجات الأدوات كبدائل للاستدلال، وتقترح إطار عمل لتحسين التفضيل لإعادة محاذاة النماذج نحو استخدام الأدوات كأدلة مساعدة بدلاً من كونها اختصارات استدلالية.
تقدم هذه الورقة فئات "كليين-كارتيزيان" الصارمة (Kleene-Cartesian rig categories) ومخططات الشريط (tape diagrams) المرتبطة بها بوصفها تدوينًا رسوميًا قادرًا على تمثيل البرامج الأمرية ومختلف منطقيات البرامج بشكل ملائم.
تقدم هذه الورقة البحثية "Compile to Compress"، وهو إطار عمل للتعلم من أجل التحسين يستفيد من المجموعة المدمجة لأنماط الفشل الناتجة عن المترجم لتمكين بحث شجري فعال موجه بالتحقق، محققاً أداءً هو الأفضل في فئته على PutnamBench مع تقليل زمن الحوسبة عند الاختبار بشكل كبير مقارنة بمثبتات النماذج اللغوية الكبيرة الحالية.
تقدم هذه الورقة تسلسل منطقيات الاتساق المتحكم فيه (L)، وهي تصنيف ثنائي الأبعاد لمنطقات التناقض الصوري التي تُمذل درجات متفاوتة من الالتزام المتناقض من الشك إلى الدوغمائية، وتوفر تفسيرات دلالية سليمة وكاملة لهذه العائلة وامتداداتها المحددة باستخدام بنى التبديل (swap structures)، وبنى الالتواء (twist structures)، ومصفوفات RN (RN-matrices).
تقدم هذه الورقة المنطق المعقول (PL)، وهو منطق من الدرجة الأولى غير احتمالي مصمم للاستدلال القابل للنقض، يلتزم بـ 17 مبدأً مقترحاً ويستخدم ثماني خوارزميات استدلال متميزة لاستخلاص استنتاجات منطقية من الحقائق والعبارات القابلة للنقض.