1215 ورقة بحثية
تقدم هذه الورقة "ألعاب النرد" (Dicey Games)، وهي إطار عمل رسمي لتحليل الأنظمة الموزعة ذات المصادر المشتركة للعشوائية، حيث تُبين أن الفرق يمكنها تحقيق احتمالات فوز مثالية تتجاوز العشوائية المستقلة من خلال التخصيص الاستراتيجي للعشوائية المشتركة الثنائية، وتُحدد خصائص وجود مثل هذه الاستراتيجيات وتمثيلها والتعقيد الحسابي لها.
تعمم هذه الورقة الهياكل الرمزية إلى نظريات أساسية تعسفية وتستفيد من خاصية النموذج الرمزي الناتجة لإثبات قابلية التقرير لعدة أجزاء من المنطق من الدرجة الأولى التي توسع الصيغ الطبقية عبر السماح بالدوال ذات الحلقات الذاتية تحت قيود محددة.
تقدم هذه الورقة امتداداً لـ Move Prover يتيح التحقق الرسمي من الدوال الأمرية من الدرجة الأولى في لغة Move عبر إدخال المحمولات السلوكية، وتسميات الحالة، واستراتيجية ترميز SMT التي تستفيد من الفصل الاستاتيكي للذاكرة في Move من أجل التحقق الفعال والاستدلال الآلي للمواصفات.
تقدم هذه الورقة إطاراً منطقياً سليماً وكاملاً، ، لنمذجة انحرافات الملفات المزدوجة (biprofile deviations) في الاختيار الاجتماعي حيث تقوم التحالفات بتغيير ملفات التقارير، وتوسع هذه النظرية المجردة عبر طبقة تدقيق مبتكرة تتميز بشهود تلاعب نمطي ومعايير للتعامل مع التوسعات خارج النطاق والحذوفات العامة.
تقدم هذه الورقة آلية تشكيل مكافأة تعتمد على الاعتقاد وصارمة مدمجة في إطار عمل مطور للتخطيط بنموذج مونت كارلو لتمكين الوكلاء المستقلين من تخليق سياسات موثوقة لأهداف المنطق الزمني الخطي (LTL) المعقدة في بيئات ذات إدراك جزئي، متجاوزةً بذلك قيود الحلول الحالية في البيئات غير اليقينية.
تقدم هذه الورقة عرضاً حديثاً، ومكتفياً بذاته، وميكانيكياً بالكامل للغة البرمجة الوظيفية LFPL ونظريتها الميتافيزيقية، حيث تقدم براهين جديدة لسلامتها واكتمالها ضمن مساعد الإثبات Istari لتوصيف القابلية للحساب في وقت حدودي.
تقدم هذه الورقة حسابات التوالي الكمية (pQLL) التي تخصص دلالات ذات قيم حقيقية للروابط الجمعية في المنطق الخطي من خلال مراجعة إطار حساب التوالي، مما يتيح مواصفات قابلة للتفاضل للأنظمة الاحتمالية وأنظمة تعلم الآلة مع إثبات حذف القطع والتمام لعائلة من الحسابات التي تتقارب إلى منطق MALL القياسي كلما اقترب معامل الصعوبة من اللانهاية.
تقدم هذه الورقة "Continuous-Eris"، وهو منطق فصل من رتبة عليا تم تنفيذه في مساعد الإثبات "Rocq"، للتحقق رسميًا من صحة خوارزميات أخذ العينات الدقيقة للتوزيعات المستمرة مثل التوزيع الطبيعي (Gaussian) وتوزيع لابلاس (Laplace)، مع معالجة القيود الأمنية والدقة الناتجة عن تقريبات الفاصلة العائمة.
تقدم هذه الورقة إطاراً فئوياً موحداً باستخدام الفئات الفعلية لترونين (Tronin) لصياغة المونادات والقوانين التوزيعية في السياقات تحت-البنيوية، مقدمةً مونادات -العملياتية و-التبادلية لبناء قوانين توزيعية معيارية تعمم النتائج الحالية وتلتقط بناءات مثل التقييمات المُفهرسة.
تقيم هذه الورقة قدرة ثلاثة نماذج لغوية كبيرة على فهم الدلالات الرسمية لمخططات تسلسل الرسائل عالية المستوى (HMSCs)، كاشفةً أنه في حين أنها تُظهر استيعاباً قوياً للمفاهيم الأساسية، إلا أن دقتها الإجمالية متواضعة (حوالي 52%) بسبب معاناتها الكبيرة مع الاستدلال الدلالي المعقد الذي يتضمن التجريد، والتركيب، والتبعية السببية.