1215 ورقة بحثية
تؤسس هذه الورقة إطاراً فئوياً موحداً يربط الحلقات التبادلية والحلقات البولية بالنظرية الجبرية الأفينية والهايبر-أفينية، على التوالي، مع تقديم توصيفات جديدة لنماذجها فوق حلقة بولية وربط النظريات الهايبر-أفينية بالجبرات البولية متعددة الأبعاد.
تقدم هذه الورقة أول لغة برمجة كمية ذات تكرار تدعم التحكم المتماسك في العمليات الكمية التعسفية من خلال تعريف دلالات تشغيلية ودلالات معنوية بناءً على امتدادات الفراغ وإثبات كفايتها والتجريد الكامل لها فيما يتعلق بتكافؤ ملاحظي جديد.
تقدم هذه الورقة البحثية **pact**، وهو نموذج تقريبي لعدّ حلول منطق التعبير عن القابلية للإرضاء (SMT) يستفيد من تقنيات التجزئة لتقدير أعداد الحلول للصيغ الهجينة بكفاءة مع ضمانات نظرية، متفوقاً بشكل كبير على النماذج المرجعية الحالية في مجموعة اختبار واسعة.
تستخدم هذه الورقة أشباه مجموعات عكسية لتوصيف حدود القابلة للعكس (تحديداً التبديلات الوراثية المحدودة واللانهائية) عبر نظريات المختلفة، مبرهنةً أن ترتيبها الطبيعي يتوافق مع توسيع ومثبتةً أن التبديلات الوراثية المحدودة تشكل العناصر القابلة للعكس في جميع النظريات الواقعة بين ونظرية موريس الملاحظاتية .
تقدم الورقة البحثية DSLean، وهو إطار عمل يبسط الترجمة ثنائية الاتجاه بين Lean 4 واللغات المخصصة لمجالات معينة الخارجية من خلال تجريد تفاصيل التنفيذ، مما يتيح التكامل السلس للمحللات الخارجية لمهام مثل الحساب الفتري، والمعادلات التفاضلية، وعضوية المثالي في الحلقات.
تقدم هذه الورقة إطار عمل جديد للتنفيذ الرمزي مُنفذ ضمن بيئة LLVM ومتكامل مع Frama-C، يقوم بتوليد عقود الدوال من خلال نقل الثوابت ومعلومات التعديل بفعالية عبر أجزاء المصفوفات المتجاورة، مما يتغلب على قيود النهج الحالية في تحليل الدوال التي تتعامل مع المصفوفات.
تؤسس هذه الورقة لتمهيدية يونيدا (Yoneda lemma) للخرائط الفائقة (categorical supermaps) لتوفير إطار عمل دقيق وغير غامض لتعميم العمليات الكمومية من الرتب العليا إلى نظريات الدوائر التعسفية، مع توضيح تطبيقها على عالم الصناديق (boxworld) والنظرية الكمومية الحقيقية.
تقدم هذه الورقة صياغة موحدة للمنطق التفاضلي والمنطق الضبابي داخل مساعد الإثبات "روك" (Rocq) باستخدام نظرية النوع المعتمد، حيث تقارن بشكل منهجي بين خصائصها التحليلية والجبرية والنظرية-الإثباتية عبر تفسيرها بواسطة الشبكات المتبقية، وصياغة أدوات الحساب الضرورية مثل قاعدة لوبيتال، وتأسيس حسابات استنتاج سليمة لكل من الأنظمة المنطقية القائمة والجديدة.
تقدم هذه الورقة إطار عمل للتحقق العصبي الرمزي يستخدم أدوات حل مسائل التبعية (SMT) وقواعد المعرفة السريرية لإجراء تدقيق رسمي وضمان الاتساق المنطقي لتقارير الأشعة المولدة بواسطة نماذج الرؤية واللغة، مما يحدد بفعالية الهلوسات والإخفاقات الاستنتاجية التي تغفل عنها المقاييس التقليدية.
تقدم هذه الورقة مفهوم المرونة في الأنظمة العشوائية، وتحديداً ضمن عمليات ماركوف لاتخاذ القرار والألعاب العشوائية، من خلال تعريف وتحليل المشكلات الأساسية المتعلقة بالاستراتيجيات التي تظل قوية ضد الاضطرابات القادرة على قلب الأفعال المقصودة، وذلك باستخدام مقاياسات كمية متنوعة لتقييم تكرار وتأثير مثل هذه الاضطرابات.