1215 ورقة بحثية
تتقصى هذه الورقة مدى حفظ تمامية كريبكي وقابلية التقرير في الاندماج المستقل لمنطقات الجهوية من الدرجة الأولى ذات المتغير الواحد، حيث تُثبت أن هذه الخصائص تظل قائمة في غياب المساواة تحت كل من دلالات النطاق المتوسع والنطاق الثابت، بينما تفشل عند إدخال المساواة والثوابت غير الصلبة بسبب ترميز المعادلات الديوفانتية، مع إثبات أيضًا أن خاصية النموذج المحدود تُحفظ فقط في الحالة المحلية.
تقدم هذه الورقة بديهيات رسومية كاملة لتباعدات كولباك-ليبلر وريني من خلال توصيفها كإثراءات كمية لفئات المصفوفات العشوائية تحت بنيتي الضرب كرونيكر والجمع المباشر ضمن إطار مخططات خيطية رسومية.
تقدم هذه الورقة نهجاً لتعلم القيود لحساب الاتصال من الدرجة الأولى الكلاسيكي، وتعمل على تحسينه بشكل تكراري، مما يقلل بشكل كبير من التراجع في بحث الإثبات غير المتوافق مع الحفاظ على الاكتمال.
تقدم هذه الورقة نهجاً جديداً لحل معادلات السلاسل المعقدة من خلال توسيع تحويلات نيلسن عبر دمج مؤثر قوة السلسلة، وصور باريك المعممة، وتفكيك المساواة.
يُعد NL2GDS إطار عمل مبتكر يسخر النماذج اللغوية الكبيرة لترجمة مواصفات الأجهزة باللغة الطبيعية تلقائياً إلى لغة وصف ترانزستور قابلة للتصنيع (RTL) ومخططات GDSII كاملة عبر تدفق OpenLane، محققاً تحسينات كبيرة في كفاءة المساحة والتأخير والطاقة مع تعميم تصميم الدوائر المتكاملة محددة التطبيقات (ASIC).
تقدم هذه الورقة لغة SCORE، وهي لغة برمجة عكسية تستخدم فضاء حالة مدعومًا بالبرهان لضمان تفسير جميع عمليات معالجة المكدس كدوال تقابلية شاملة، مما يتغلب على قيود نهج التقابل الجزئي التقليدي ويُمكّن من دراسة التعقيد الحسابي في النماذج العكسية بالكامل.
تقدم هذه الورقة نظرية معادلات مبتكرة لحساب I تعتمد على "أشجار أوهانا" (Ohana trees) التي تتبع المتغيرات الخفية أو اللانهائية، وتثبت مبرهنة تبادل بين هذه الأشجار وتوسعات تايلور، وتوفر نموذجاً دلالياً علاقيًا غير متطابق (non-idempotent relational denotational model) لاستيعاب هذا المفهوم المنقح للمساواة.
تقترح هذه الورقة إطاراً هندسياً مبتكراً ينمذج استدلال النماذج اللغوية الكبيرة كتدفقات سلسة في فضاء التمثيل، مُثبتةً من خلال تجارب تجريبية أن التنبؤ بالرمز التالي يُمكّن النماذج من استيعاب الثوابت المنطقية كهندسة من رتب عليا، مما يتحدى فرضية "الببغاء العشوائي" ويشير إلى وجود قانون تمثيلي عالمي يكمن وراء الفهم الآلي.
تقدم هذه الورقة مكتبة Agda متاحة للعموم تُنفذ تقنيات اسمية للتعامل مع الأسماء وربط المتغيرات، حيث توازن بنجاح بين الصياغة الرياضية الصارمة ومتطلبات الأعباء التشغيلية العملية.
تُظهر هذه الورقة القدرة التعبيرية للجمع بين الاستقراء العودي الهيكلي (structural corecursion) وعوامل التحكم الكلاسيكية مثل `callcc` من خلال تقديم برهان استقرادي عودي جديد لمبدأ الحمام اللانهائي (Infinite Pigeonhole Principle) وتنفيذ لمبدأ بديهية الاختيار القابل للعد (Axiom of Countable Choice) يبرر التوقف عبر التكرار العودي المشترك (coiteration) وحده، مما يباين مناهج تمرير الاستمرارية (continuation-passing) التقليدية التي تعتمد على حجج توقف خارجية.