1215 ورقة بحثية
تقدم هذه الورقة SuperDP، وهي طريقة مؤتمتة بالكامل وسليمة لدحض الخصوصية التفاضلية من نوع في الآليات العشوائية ذات التوزيعات المنفصلة والمستمرة، وذلك عبر البحث المتزامن عن المدخلات المنتهكة ودالة تمييز باستخدام السوبرمارتينجال (supermartingales) والسابمارتينجال (submartingales).
تؤسس هذه الورقة نظرية عامة للتعبير والبديهيات للنماذج المجمعة (bundled modalities) من خلال تقديم تعريف موحد للتماثل المتبادل (bisimulation)، وفئة خاصة من الحزم المحدبة، وبديهيات ملموسة لمختلف السيناريوهات المعرفية.
تقدم هذه الورقة معامل "بوابة البرهان" (proofdoor)، وهو إطار عمل للتفكيك يربط بين تجزئة البنود والمستدخلات، لتفسير وإثبات أن حلول (CDCL) لمسائل الإرضاء (SAT) تحل مسائل تحقق الدوائر المحددة بكفاءة من خلال إظهار أن الصيغ ذات "أبواب البرهان" الصغيرة تقبل براهين تحليلية قصيرة يمكن حسابها في وقت حدودي، مع تسليط الضوء أيضاً على حساسية هذا الإطار لخيارات التفكيك.
توضح هذه الورقة القصيرة الجهود الجارية لتعزيز ثقة المستخدم في مبرهن النظريات الآلي Vampire من خلال إعادة بناء براهينه كبراهين موثوقة داخل مساعد الإثبات Lean.
توسع هذه الورقة نطاق نمذجة وتدقيق بروتوكولات التعلم الاتحادي عبر توسيع نظام النوع الجلسي التصاعدي غير المتزامن من خلال إدخال عمليات إدخال وإخراج متعددة المشاركين وعلاقة نوع فرعي مخصصة، مع إثبات السلامة، وخلو الجلسات من المآزق، والحيوية، ودقة الجلسة بشكل رسمي.
تقدم هذه الورقة صياغة رسمية لنظرية جيلفوند-شنايدر، التي تحل مسألة هيلبرت السابعة من خلال إثبات أن عدد متسامٍ في لغة Lean 4 عندما يكون جبرياً بحيث و عدداً جبرياً غير نسبي.
تقدم هذه الورقة ترميزاً حقنياً بحجم خطي للسلاسل المحدودة إلى الأعداد الطبيعية باستخدام متتالية فيبوناتشي مقسمة إلى كتل، تحقق نمواً مثالياً من رتبة مع تجنب التضخم الأسي المتأصل في طريقة روسكو للتقفيل الثنائي عديم الحمل.
تُثبت هذه الورقة أن أي دالة متعددة القيم يمكن تمثيلها بواسطة حدود لامدا خطية ضمن نظام نوع متعدد الأشكال من الدرجة الثانية باستخدام أساليب تشبه الدوائر وأساليب استقرائية، مع استكشاف التحسينات والتطبيقات العملية أيضًا.
تقدم هذه الورقة صياغة لمصفوفات طوبولوجيا الشبكة (المجاورة، والدرجة، ولابلاس، والوقوع) ضمن مساعد الإثبات Isabelle/HOL استناداً إلى الرسوم البيانية الموجهة، حيث يتم التحقق من الخصائص الكلاسيكية والعلاقات بين المصفوفات لدعم التحليل الدقيق للأنظمة مثل الشبكات الكهربائية من خلال أمثلة مثل اختزال كرون والتحقق من تبدد القدرة.
تؤسس هذه الورقة تقابل ستون للمونادات عبر تقديم تزاوج متناظر (idempotent adjunction) متغاير الاتجاه بين المونادات المرتبة (ranked monads) على فئة والفئات الداخلية في المواقع (locales)، وهو ما يتقيد بتقابل ستون الكلاسيكي ويُوصّف المونادات أحادية التعيين-فائقة الأفينية (hyperaffine-unary monads) باعتبارها النقاط الثابتة المقابلة للفئات الموضعية الوافرة (ample localic categories).