1215 ورقة بحثية
تقدم هذه الورقة أول خوارزمية تقوم، بمعطى جملة رتبة أولى موجبة، بحساب شكلها المكافئ منطقياً ذي العرض الأدنى عبر تطبيق مجموعة محددة من قواعد إعادة الكتابة النحوية، مما يؤسس فهماً خوارزمياً كاملاً لتقليل العرض من خلال تقارب نظريات إعادة كتابة الحدود، وتقييم الاستعلام، والتفكك البنيوي.
تقدم هذه الورقة نهجاً هجيناً جديداً يجمع بين تحليل تتبع التدفق القائم على تحويل الرسم البياني الساكن والتحقق الديناميكي للكشف المنهجي عن ثغرات التحكم في الوصول المكسور، المباشرة وغير المباشرة، في واجهات برمجة تطبيقات الرسوم البيانية (Graph APIs)، كما هو موضح من خلال تطبيقه على واجهة برمجة تطبيقات GitHub GraphQL.
تقدم الورقة البحثية FATE، وهي سلسلة معيارية جديدة للجبر الصوري تمتد من التمارين الجامعية إلى مشكلات بحثية بمستوى الدكتوراه، والتي تكشف أن النماذج اللغوية الكبيرة الحالية تعاني بشكل كبير في صياغة الاستدلال الرياضي المتقدم، محققة دقة تقارب الصفر في المهام الأكثر صعوبة رغم أدائها القوي في اللغة الطبيعية.
تقترح هذه الورقة أول تكييف لنظرية كورسيل (Courcelle's Theorem) للرسوم البيانية الزمنية يتجنب الاعتماد الصريح على مدة الحياة، وتُقدم مفهوم المشتق عبر نافذة زمنية منزلقة لتعريف عرض الشجرة (tree-width) وعرض التوأم (twin-width)، وتضع نظريات عليا لمنطق زمني قادر على حل مشكلات متنوعة مثل الكليكات الزمنية (temporal cliques).
تقترح هذه الورقة نهجاً مبتكراً لاستخراج المواصفات الزمنية المدركة للبيانات من آثار التنفيذ عبر الجمع بين التركيب الموجه نحو بناء الصيغ (Syntax Guided Synthesis) وتفسير البادئة المحدودة لمنطق التدفق الزمني (TSL)، مما يتيح التركيب القوي وذي الكفاءة في استهلاك العينات للبرامج التفاعلية التي تجمع بين تحويلات البيانات والسلوكيات الزمنية.
تقارن هذه الورقة بين ثلاثة نماذج دلالية ثابتة الأبعاد لرضا المنطق الكمي — دلالات هيلبرت-الشبكية القياسية، ودلالات المُسقط المتعامد عالمياً، ودلالات البولينية الجزئية المحلية — حيث تثبت وجود تسلسل هرمي صارم تكون فيه الدلالات القياسية أكثر تعبيراً من غيرها، كما يتضح من خلال صيغة صريحة تكون قابلة للإرضاء في الدلالات القياسية ولكنها غير قابلة للإرضاء تحت الدلالتين الأخريين لجميع الأبعاد .
تقدم هذه الورقة LLM2SMT، وهي دراسة حالة تثبت أن وكيل برمجة يعتمد على نموذج لغوي كبير (LLM) يمكنه بناء حل SMT كامل وتنافسي من طراز DPLL(T) لـ QF_UF بشكل مستقل — بما في ذلك خوارزمية Nieuwenhuis-Oliveras للإغلاق التطابقي وانبعاث براهين Lean — دون أي كود مكتوب بشرياً.
تقترح هذه الورقة استخدام الشبكات العصبية الرسومية للتنبؤ بترتيبات التفرع الأولية لمحللات SAT من نوع CDCL، مما يظهر تسريعاً كبيراً في الاختبارات المعيارية العشوائية وشبه الصناعية مع ملاحظة أن هذا النهج يعاني مع الحالات الصناعية المعقدة بسبب تجاوز الاستدلالات الديناميكية للمحلل للتنبؤات.
تقدم هذه الورقة قواعد بيانات موجهة بالرسوم التخطيطية (sketch-oriented databases)، وهي إطار عمل فئوي يوحد مختلف النماذج والميزات القائمة على الرسوم البيانية من خلال رسوم تخطيطية ذات حدود منتهية، مع اقتراح محددات موضعية للاستدلال المساري الكسول ورسوم تخطيطية متقطعة لتمكين التركيب التركيبي والنمو القابل للتوسع للنماذج.
تقدم هذه الورقة أعمال المؤتمر الدولي الثامن لنظرية الفئات التطبيقية (ACT2025)، الذي عُقد في جامعة فلوريدا في يونيو 2025، والذي ضم مجموعة متنوعة من المساهمات التي شملت تخصصات نظرية وتطبيقية مثل علوم الحاسوب، والحوسبة الكمومية، والكيمياء.